A "proof" of Fermat's Last Theorem that fits the margin
21 days ago
- Fermat claimed a proof of his Last Theorem but never wrote it due to margin constraints.
- Anthropic formalized Fermat's Last Theorem with 13 million lines of Lean code.
- A bug in Lean's String.Pos.Raw.extract causes a mismatch: logical evaluation yields empty string, native evaluation returns the full string.
- This contradiction allows proving anything, including Fermat's Last Theorem, in Lean.
- The Lean team fixed the bug quickly: a memory-safety fix in ~90 minutes, semantic mismatch fixed in 5 days.
- The extra axiom native_decide adds the compiler to the trusted boundary, requiring careful use.
- More work (e.g., lean4lean, alternative kernels) is needed to ensure proof correctness against such exploits.