Fermat's Last Theorem in Lean 4
A team of researchers has formalized the proof of Fermat's Last Theorem in the Lean 4 theorem prover, extending the earlier Lean 3 version. The new formalization uses Lean 4's improved language features and performance, enabling a more concise and maintainable representation of the theorem's complex arguments. This milestone demonstrates Lean 4's growing capability for large-scale formal mathematics.