3 ms·
Out of these 100 famous theorems, only 33. Fermat's Last Theorem has yet to be proven in a formal system. It's like Formal's Last Theorem :-)
by tromp 3y ago
Out of these 100 famous theorems, only
33. Fermat's Last Theorem
has yet to be proven in a formal system. It's like Formal's Last Theorem :-)
- matthewfelgate 3y agoLOL
- pitdicker 3y agoGood look to whomever is going to formalize that! Does anyone have an idea of the amount of effort it would take? Would the effort be comparable with the original proof by Andrew Wiles?
- mazsa 3y ago"Here is a list of some of what has been written about this or things we can do:" https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theorem https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theore...
- dvh 3y agoIf HN had slightly wider margin it could easily fit there.
- hansbcarlsen 3y agoi rarely comment here.
- kevinwang 3y agoApparently a few years: https://x.com/XenaProject/status/1712488019016515662?s=20 https://x.com/XenaProject/status/1712488019016515662?s=20
- muldvarp 3y agoProf. Kevin Buzzard got a research grant for formalizing FLT in Lean. https://twitter.com/XenaProject/status/1712488019016515662 https://twitter.com/XenaProject/status/1712488019016515662
- mikhailfranco 3y agoCircling the last survivor?