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

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.