logoalt Hacker News

jrflotoday at 7:06 PM2 repliesview on HN

Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?


Replies

mswphdtoday at 9:50 PM

not really. it's one of the most difficult ones so far for sure, but pales in comparison to something like the classification of finite simple groups.

This was initially "completed" in the 80s. You can see the timeline for cleaning up the proof in e.g. this mathoverflow answer

https://mathoverflow.net/questions/114943/where-are-the-seco...

it's something that some people have been waiting decades for, and is not yet completed.

bjournetoday at 7:23 PM

Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.

show 2 replies