Lean 证明无人读得懂：密码学家呼吁为 AI 形式化证明建高层语言
jedisct1 · x · 2026-10-14
Symbolic Software 的 Nadim Kobeissi 发表 IACR 论文《Nobody Will Read the Lean: A Case for High-Level Cryptographic Languages》，指出 AI 形式化证明带来新的根本问题：没人读证明本身了。
要点：
- 2026 年 9 月，AI 用 11 天完成费马大定理的 Lean 证明，AI 证明器已开始触及密码学；几年内可能产出机器验证的「Signal 安全」证明，但 Lean 无法检验定理是否表达了你想表达的——这取决于 AI 同样撰写的定义。
- 已有先例：某 Lean 库的 Schnorr 签名安全性定理通过了检查器，但按其写法对所有敌手都成立，等于什么也没承诺。
- 证明变廉价后，稀缺资源是能读懂被证明了什么的人；作者主张协议所有者亲自撰写简短可读的模型，并像 AES 那样公开、版本化地约定前向安全等协议目标定义——实测一页 Verifpal 模型在换用其他标准定义时，五个判定中有两个会翻转。
- 定义共识需要多年公开辩论，更好的证明器无法缩短这一过程，因此应现在开始。
「安全」频道最新
- AI agent 自主挖出 V8 沙箱逃逸链:只需一句人类提示 — moyix · 2026-10-15
- Anthropic 招 AI 安全研究员:周薪 3850 美元无需经验 — AIFlow_ML · 2026-10-15
- moyix 复盘 AI agent 挖洞：找到一个可用漏洞后就不再探索 — moyix · 2026-10-15
- Rivian电动车每周悄悄上传8GB数据，车主质疑数据收集规模 — generativist · 2026-10-15
- 威尔斯议员被曝用智能眼镜当提词器,议会要求紧急立规 — nordicinst · 2026-10-15
- Peter Yang 分享完整 prompt：让 AI 代理向数据商批量提交删除/退出请求 — petergyang · 2026-10-15