How Lean Formalized Fermat’s Last Theorem
Fermat’s Last Theorem has moved from a handwritten conjecture to a massive Lean formalization checked by a computer kernel. This beginner-friendly guide explains proof assistants, Wiles’s strategy, AI collaboration, and the limits of machine verification.