Vitalik：應嘗試創建新型「可讀性證明語言」以提升人類理解 AI 生成證明
日期：2026年7月21日 下午11:20PANews 7月21日消息，Ethereum 聯合創始人 Vitalik Buterin 提出，應探索一種可編譯為 Lean、HOL 等定理證明係統的新型高級編程語言，重點優化「定義與定理」的可讀性，而非證明過程本身。Vitalik 稱，該語言的目標場景是 AI 輸出大規模形式化證明後，幫助人類清晰理解這些證明究竟「形式化地證明了什麼」，即讓讀者更容易審視與核查 AI 所給出的具體數學與邏輯主張。
内容來源：PANews
