9 ms·
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 https:
by wiz21c 2mo 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 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.")
- jfengel 2mo agoEnormous. 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.