Vitalik提議開發支持AI生成証明的高級語言

BiRun 消息，以太坊聯閤創始人 Vitalik Buterin 提議開發一種可編譯至 Lean、HOL 等形式化驗証系統的高級語言。該語言旨在提昇定義和定理的人類可讀性，而非專注於証明過程本身。Vitalik 設想的應用場景是由 AI 生成大規模形式化証明，再通過這種高級語言進行表達與驗証，從而降低形式化數學的門檻，促進 AI 在嚴謹邏輯推理領域的應用。這一提議結閤了加密貨幣社區對形式化驗証的重視與 AI 技術的發展趨勢，有望推動智能閤約安全性及數學証明自動化的進步。