新语言定位：AI 写证明，人类审结论
以太坊联合创始人 Vitalik Buterin 近日提出一种全新的编程语言构想，该语言将直接编译至 Lean 或 HOL（另一款形式化证明助手），其核心目标在于解决人工智能输出大规模自动化证明时人类难以快速验证的难题。随着 AI 生成证明的速度已远超人类团队手工编写，但鲜有读者能立即确认这些证明实际确立了哪些结论。
背景：证明助手的六十年与以太坊的实践
Lean 是一款数学家和工程师用于编写可逐行计算机校验证明的软件。以太坊研究团队已在使用它验证加密代码和共识逻辑。尽管证明助手问世近六十年，该领域始终小众。Buterin 在博文中指出，证明的内部步骤仅需满足数学正确性这一要求，读者无需直接检查这些机制；而定义和定理则截然不同，人类需要阅读它们以了解软件的实际保证。
从双版本分离到以太坊自身重建
在一篇今年5月的博文中，Buterin 探讨了类似的分离思路：数学证明确保高效底层代码与独立可读规范相匹配，从而一次审计同时覆盖两个版本。这一时间点恰好与以太坊自身的重建努力相呼应——被称为“Lean 以太坊路线图”。研究人员正使用类似方法构建一个形式化验证的 ZK-EVM（零知识可证明版本的以太坊虚拟机）。
AI 工具已能编写 Lean 证明
大型语言模型目前已经可以编写可用的 Lean 证明。Buterin 点名 Claude 与 Deepseek 4 Pro 为有效工具，此外还有专为 Lean 微调的小模型 Leanstral。实例项目 evm-asm 是一个已验证的可读参考实现的 EVM 实现。这一能力体现了开发者们在近期 Buterin 的 AI 挑战中展示的推理技巧——测试者数小时内即解决挑战。
安全考量：形式化验证抵御 AI 攻击激增
其意义远超便利性。安全研究人员追踪到今年 AI 辅助的漏洞利用尝试显著增长。形式化验证代码可为这一趋势提供防御。一个更友好的规范语言能让开发者在审查声明时不必穿梭于冗长的证明代码中。Buterin 持续公开展示这些想法，例如他最近演示的基于零知识证明的匿名公告牌，展示了可验证声明如何从研究仓库走向实际产品。研究人员还在 Lean 中形式化验证共识客户端以尽早发现漏洞。
方向明确，实现待定
这一思路遵循熟悉的模式：将快速代码与可读声明分离，然后证明两者匹配。目前新语言尚无原型，Buterin 也未确定具体语法。开发者们可能逐渐趋同于一个统一标准，也可能形成多个不兼容的方言。这一选择将决定 AI 验证代码能够多快进入生产系统。
免责声明：以上内容(如有图片或视频亦包括在内)均为平台用户上传并发布，本平台仅提供信息存储服务，对本页面内容所引致的错误、不确或遗漏，概不负任何法律责任，相关信息仅供参考。
本站尊重他人的知识产权、名誉权等法律法规所规定的合法权益!如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到qklwk88@163.com，本站相关工作人员将会进行核查处理回复
