Trail of Bits 发现 Lean 漏洞，20 行假证明骗过费马大定理

Anthropic 上周用 1300 万行 Lean 代码完成了费马大定理的完整形式化，但安全公司 Trail of Bits 的研究员 Marc Ilunga 随即披露 Lean 4 的一个漏洞：利用 String.Pos.Raw.extract 函数中逻辑定义与编译实现不一致的缺陷，仅需约 20 行（一说 13 行）代码就能构造出通过校验的假证明，「证明」同一定理。这一发现引发了对形式化验证工具本身可靠性的关注。

2026-09-09 ~ 2026-09-10 · 2 条相关

• 13百万行证明被20行推翻:Trail of Bits发现Lean漏洞戏耍费马大定理 — CatAstro_Piyush · 2026-09-09
• Trail of Bits 发现 Lean 漏洞,13 行假证明能通过费马大定理校验 — jedisct1 · 2026-09-10