洞察：Vitalik Buterin 提出一種新的程式語言。它能編譯成像 Lean 這樣的證明系統，且只為了讓定義與定理對人類而言達到盡可能的可讀性而設計。

推理的關鍵翻轉了通常的瓶頸。「在證明裡，真正重要的是證明必須正確。」機器會檢查這一點。人類需要的是理解「實際上已被證明的精確主張是什麼」。
AI 證明器已經在運行 Lean。AlphaProof、DeepSeek-Prover 以及 Mistral 的 Leanstral 都把它作為其形式化後端，AWS 也會在其中正式驗證其授權語言，而 Microsoft 則用它來驗證產線等級的密碼學。
最近，有 10 個 AI 代理在一個週末內建立了一種具驗證能力的語言，並附帶已證明的最佳化，零行由人類手寫的程式碼。現在，證明的交付速度比任何人閱讀它們所聲稱的內容都更快。
@VitalikButerin 長年來一直推動形式化驗證，視其為應對智慧合約漏洞攻擊的答案，而以太坊基金會也在運作一項專門的驗證工作。
人類可讀的定理層，正是該議程中缺失的拼圖；審計人員終於能夠閱讀 AI 已驗證的合約實際保證了什麼。