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