> 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.