In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type.
If the compiler certifies that the code indeed produces a term of that type, then the proof is correct.
So, only need to trust:
(1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really)
If the compiler certifies that the code indeed produces a term of that type, then the proof is correct.
So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really)
(2) Lean compiler is correct