Comment by wiz21c
9 hours ago
I'm not a mathematician and AI doesn't answer very well. Could someone tell us how big an endeavour this is: https://github.com/ImperialCollegeLondon/FLT ?
(the site is : "An ongoing multi-author open source project to formalise a proof of Fermat's Last Theorem in the Lean theorem prover.")
Enormous.
Wiles' proof is 129 pages long, and builds on results that require a vast amount of infrastructure to define.
It's going to take dozens of person-years.