13百万行证明被20行推翻:Trail of Bits发现Lean漏洞戏耍费马大定理
CatAstro_Piyush · x · 2026-09-09
Anthropic 上周用 1300 万行 Lean 代码完成了费马大定理的完整形式化,而安全公司 Trail of Bits 声称用 20 行代码就「证明」了同一定理——方法是利用他们发现的一个 Lean 4 缺陷。
关键事实:
- 缺陷位于 String.Pos.Raw.extract(底层字符串切片函数):当在极大位置提取单字节切片时,Lean 的逻辑定义返回空字符串,但编译后的原生代码返回整个原字符串。把两种求值结果组合,即可在 Lean 内制造矛盾,让任意荒谬命题获得 ✓。
- 该问题影响截至 4.33.1 的所有稳定版 Lean,已在 v4.34.0-rc1 修复。
- Trail of Bits 强调这不是内核 soundness 问题;他们是在用 GPT-5.6 试验新的代码审查 skill 时发现的这个 bug。
费马当年说自己「页边太窄写不下绝妙证明」,Trail of Bits 调侃:看来 20 行确实放得下。
所属事件:Trail of Bits 发现 Lean 漏洞，20 行假证明骗过费马大定理(2 条相关)→
「Fun」频道最新
- AI 圈梗图：Anthropic、OpenAI「互杀」，苹果还在折叠屏 — ChengleiSi · 2026-09-10
- 程序员自嘲梗：嗑再多 Adderall 也写不过 LLM，如同阿姆斯特朗遇上电动车 — generativist · 2026-09-10
- 网友恶搞 Anthropic 财报电话会：AI 灭绝风险成了「长期 ARR 增长挑战」 — thedealdirector · 2026-09-10
- OpenAI 员工自嘲式一句话:「我觉得 AI 可能会灭掉所有人」 — Miles_Brundage · 2026-09-10
- 用 GPT6Astra 在 Blender 里重建音乐视频，效果实拍 — Alzeric · 2026-09-10
- 把推特链接放上简历,确保自己是「文化合适」的员工 — haydendevs · 2026-09-10