Anthropic publishes machine-checked proof of Fermat's Last Theorem in Lean 4
Anthropic has released a complete, machine-checked proof of Fermat's Last Theorem in the Lean 4 theorem prover, built on Mathlib. The proof follows the classic Frey–Serre–Ribet–Wiles–Taylor–Wiles argument and is verified by Lean's kernel, the independent Rust-based kernel nanoda, and the comparator tool. The repository includes 60,475 modules, 29,511 theorems, and a browsable HTML version of the proof. It's a research artifact, not maintained, and not accepting contributions.
Together, these checks establish that the statement above follows from the three axioms, given trust in the Lean kernel (or nanoda) and the checking tools.