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