Comment by EGreg
8 hours ago
So Fermat’s Last Theorem has been proven a long time ago? By Andrew Wiles right? Is this like Appel and Haken >>> Seymour and Robin Thomas proof of 4CT?
8 hours ago
So Fermat’s Last Theorem has been proven a long time ago? By Andrew Wiles right? Is this like Appel and Haken >>> Seymour and Robin Thomas proof of 4CT?
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.