Trail of Bits finds Lean bug that lets a bogus Fermat's Last Theorem proof pass verification
jedisct1 · x · 2026-09-10
Trail of Bits researcher Marc Ilunga disclosed a quirky Lean 4 bug: String.Pos.Raw.extract disagrees between its logical definition (returns empty string for an astronomically large one-byte slice) and the compiled native code (returns the entire original string). Combining the two evaluations lets an absurd "proof" of Fermat's Last Theorem pass Lean's full checker on versions up to 4.33.1.
Key points:
- Found while experimenting with a code-review skill using GPT-5.6
- The team clarifies this is not a kernel soundness issue
- Patch is included in v4.34.0-rc1
- Timely joke: Anthropic recently formalized FLT with 13 million lines of Lean
More from Fun
- The meme of 'informing' Claude Opus 3 about recent AI progress — repligate · 2026-09-10
- Chinese model caught distilling via API relay, turns out it was distilling itself — teortaxesTex · 2026-09-10
- Liang Wenfeng Stars in a Promo Video for DeepSeek V4.1 Flash, Complete With a Catgirl — teortaxesTex · 2026-09-10
- Blogger's Apple autopsy: Vision Pro flop, Apple Car dead, Siri 'dumb' for 15 years — oran_ge · 2026-09-10
- Defending DHH's Omarchy: Linux for the masses needs a great terminal, like macOS had BSD — bytebot · 2026-09-10
- "If you're using Codex Spark, you're down very very bad": dev mocks OpenAI's tool — CtrlAltDwayne · 2026-09-10