Vitalik 提議開發可編譯為 Lean 的高級編程語言，以提昇 AI 証明的可讀性

深潮 TechFlow 消息，7 月 21 日，據 Vitalik Buterin（@VitalikButerin）發文表示，其建議開發一種新型高級編程語言，該語言可編譯為 Lean（或 HOL 等形式化驗証工具），覈心目標是讓人類儘可能輕鬆地閱讀定義與定理內容（而非証明本身）。其設想的使用場景為：AI 負責輸出証明內容，而該語言則幫助讀者快速理解 AI 所証明的具體命題。