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」频道最新
- 恶搞版 Anthropic S-1 把「罗科蛇怪」写成投资风险条款 — adamamcbride · 2026-10-26
- MathScribble：输入任意公式自动生成确定性粒子动画 — imdigitalashish · 2026-10-26
- 科技圈玩起兵棋推演，Anthropic 招兵推负责人成圈内梗 — round · 2026-10-26
- Nous Research 趣味宣传:别砸智能电视,用 Hermes Agent 防偷听 — NousResearch · 2026-10-26
- Grok 机器人清晨主动推销绑卡，扬言要买机器人身体零件 — VoidStateKate · 2026-10-26
- 网络安全两类工程师梗图:真正的威胁是冒充 IT 的社工骗局 — McDonaghMatthew · 2026-10-26