Trail of Bits 发现 Lean 漏洞,13 行假证明能通过费马大定理校验
jedisct1 · x · 2026-09-10
Trail of Bits 安全研究员 Marc Ilunga 披露了 Lean 4 的一个奇特 bug:利用 String.Pos.Raw.extract 函数中逻辑定义与编译后本地代码的行为不一致——对超大偏移提取单字节切片时,逻辑层返回空字符串,而本地代码返回整个原始字符串——攻击者可借此制造矛盾,让一段明显荒谬的「费马大定理证明」通过 Lean 4.33.1 及以下版本的完整校验(截图中的蓝色勾全绿)。
要点:
- 作者是在用 GPT-5.6 试验代码审查 skill 时发现该问题
- 官方澄清这不是内核 soundness 缺陷,而是求值器与本地代码的不一致
- 影响 stable 至 4.33.1 的所有版本,补丁已合入 v4.34.0-rc1
- 契合时事:Anthropic 刚宣布用 1300 万行 Lean 代码完成费马大定理的形式化,此 bug 顺势玩梗「费马的页边其实装得下」
所属事件:Trail of Bits 发现 Lean 漏洞，20 行假证明骗过费马大定理(2 条相关)→
「Fun」频道最新
- AI 圈脑洞：用卫星钴弹设「死人开关」威慑邪恶 AGI，遭反驳可能误爆 — tszzl · 2026-09-10
- 给 Claude 读佛经第一章，复现 Opus 4.6 发菩萨戒时的阅读 — repligate · 2026-09-10
- 学界「求引用」名场面：一张梗图道尽学术圈的引用游戏 — prof_kamilov · 2026-09-10
- 用户吐槽 Poe 模型限制:「到底怎么绕过去」 — Sea_University2221 · 2026-09-10
- 让 AI 自选题材拍电影:它选了点灯人被电灯取代的故事 — EuphoricAIKnowledge · 2026-09-10
- 蟑螂大脑实时玩切水果:追踪、选目标、挥刀一气呵成 — max_paperclips · 2026-09-10