Re:Formalizing Fermat's Last Theorem
by latent-person on Saturday September 05, 2026 @08:19AM
(#49575828)
From the article:
> The finished proof was checked by Lean; it uses just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT.
So it proved the statement of FLT made independently in Mathlib. So no reason to not trust it proved the correct thing.
> The finished proof was checked by Lean; it uses just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT.
So it proved the statement of FLT made independently in Mathlib. So no reason to not trust it proved the correct thing.