Trail of Bits finds Lean bug that fakes Fermat's Last Theorem proof in 20 lines

Days after Anthropic formalized Fermat's Last Theorem in 13 million lines of Lean, Trail of Bits researcher Marc Ilunga disclosed a Lean 4 bug allowing a bogus proof of the theorem to pass verification in roughly 20 lines, raising concerns about formal verification tooling itself.

2026-09-09 ~ 2026-09-10 · 2 related posts

• Trail of Bits 'proves' Fermat's Last Theorem in 20 lines via a Lean 4 bug — CatAstro_Piyush · 2026-09-09
• Trail of Bits finds Lean bug that lets a bogus Fermat's Last Theorem proof pass verification — jedisct1 · 2026-09-10