BlockWeeks 7月22日消息，以太坊联合创始人 Vitalik Buterin 提议创建一种新型高级编程语言，该语言可直接编译为 Lean 或 HOL 等形式化证明助手，旨在解决 AI 生成的大量自动化证明难以被人类快速验证的问题。Buterin 表示，该语言专注于让人类轻松阅读定义和定理，而非证明本身，从而弥补当前 AI 输出与人类审查之间的 gap。此提案与以太坊的 “Lean 以太坊路线图” 以及形式化验证 ZK-EVM 的努力相呼应，但尚无原型或具体语法。（本快讯由 BlockWeeks 编译整理自公开信息）
