Comment by kzrdude

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.