Hacker News Reader

Prof. Kevin Buzzard got a research grant for formalizing FLT in Lean.

Circling the last survivor?

Good 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?

If HN had slightly wider margin it could easily fit there.

i rarely comment here.

"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-Theore...

LOL