What if the mathematical objects are not encoded "correctly"?
For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?
that's something a human needs to do, and it's non trivial, but it's a simple task compared to checking the correctness of the proof. in any case, most of the language is probably already defined in Lean and checked independently by many people.
I think the other commenters are right, as long as the statement of FLT is correct and no funny stuff is used (admitting theorems without proof or defining new axioms) then it doesn't matter what you used in the proof.
For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?