|
|
|
|
|
|
by wiz21c
15 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.") |
|
|
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.