A “proof” of Fermat’s Last Theorem that fits the margin
Trail of Bits described a Lean bug affecting String.Pos.Raw.extract, the language's low-level string-slicing function, present in all stable versions of Lean up to 4.33.1, with a patch incorporated in v4.34.0-rc1. When asked to extract a one-byte slice at an astronomically large position, Lean's logical definition returns the empty string, while the compiled native code returns the entire original string. That disagreement is enough to manufacture a contradiction: Lean's ordinary evaluator "proves" the tiny slice was empty, while native evaluation "proves" the same slice contained "a truly marvelous proof." Combined, Lean concludes the empty string equals a non-empty string, and from a contradiction anything follows, including Fermat's Last Theorem. The post shows a "checked" proof of Fermat's Last Theorem using Lean 4.33.1 with blue checkmarks, and notes the issue was found while using GPT-5.6 to experiment with a new skill for code review. The post states the issue is not a kernel soundness issue. About 90 minutes after the report, hargoniX opened a fix for the memory-safety problem, merged roughly three hours after filing; Rob23oba fixed the remaining semantic mismatch five days after the report, closing the issue. The post notes that #print axioms flt shows 'flt' depends on axioms: [propext, Classical.choice, Quot.sound, flt._native.native_decide.ax_1_1], and that native_decide adds the compiler to the trusted boundary. It also references Anthropic's announcement of a complete formalization of Fermat's Last Theorem using 13 million lines of Lean code, and points to Lean's guidance for validating a Lean proof, plus lean4lean and alternative kernel implementations as further work.
Developers relying on Lean proofs should note that native_decide adds the compiler to the trusted boundary, so proofs can be accepted through tooling issues rather than kernel soundness.