FLT was proven in 1995 by Andrew Wiles (with help of Richard Taylor). This is not even a new proof, or at least they don't claim that it is. It's the formaliza

FLT was proven in 1995 by Andrew Wiles (with help of Richard Taylor). This is not even a new proof, or at least they don't claim that it is. It's the formalization (in Lean) of an existing proof. That means, they are 'porting' the proof to a theorem proving programming language.