A “proof” of Fermat’s Last Theorem that fits the margin

Summary: Trail of Bits found a bug in Lean's low-level string-slicing function, String.Pos.Raw.extract, where extracting a one-byte slice at an astronomically large position returns the empty string in Lean's logical definition but the entire original string in compiled native code. That disagreement produces a contradiction that lets Lean accept a "checked" proof of Fermat's Last Theorem, and the issue affects all stable versions up to 4.33.1, with a fix merged about three hours after filing and the remaining semantic mismatch closed five days later.
What's compelling: The exploit relies on the native_decide axiom, which adds the compiler to the trusted boundary, so a machine-checked proof can be deemed correct through a prover bug rather than sound reasoning. Fermat's theorem took 350+ years to prove; the Lean team patched this one in roughly three hours, but the same class of gap sits under any proof you accept without checking its axioms.

Read the original at Trail of Bits Blog ↗