Vitalik Buterin 提出新型专用语言，桥接AI生成证明与人类可读性

以太坊联合创始人 Vitalik Buterin 近日提出一种全新编程语言构想，可直接编译为 Lean 或 HOL 等形式化证明助手支持的格式，旨在解决AI大规模生成数学证明后人类难以理解的问题。该语言强调内部推理步骤只需数学正确性，而定义与定理部分必须清晰可读。此提议与以太坊社区推进的“Lean Ethereum”路线图高度契合，研究人员正利用 Lean 构建形式化验证的 ZK-EVM 和共识客户端。Buterin 指出，应形成“AI写证明、人类查主张”的模式，以应对日益增多的AI辅助攻击。目前新语言尚无原型，但相关理念已进入实际产品展示，如基于零知识证明的匿名广告牌系统。