據 Woofun AI 消息，以太坊聯合創始人 Vitalik Buterin 提出一種新型高級編程語言構想。該語言可編譯爲 Lean 或 HOL 等格式，核心設計目標是優化定義與定理的人類可讀性，而非證明過程。