6 ms·

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

by jrflo 12d ago

bjourne 12d ago
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.
- simpaticoder 12d ago
  But isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?
- bigstrat2003 12d ago
  > Now we add an LLM to that list. No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.
  - bjourne 12d ago
    A meme free of charge for you, sir: https://www.reddit.com/r/singularity/comments/1jl5qfs/its_just_predicting_tokens_v2/ https://www.reddit.com/r/singularity/comments/1jl5qfs/its_ju...
- traes 12d ago
  25-50 seems like a pretty lowball estimate, I guess depending on your definition of "understand."
mswphd 12d ago
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-second-and-third-generation-proofs-of-the-classification-of-fin/217397#217397 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.

6 ms·

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

by jrflo 12d ago

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

bjourne 12d ago
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.
- simpaticoder 12d ago
  But isn't that understanding discarded? It is if you mean "intermediate working state" while it was generating the LEAN code. Which raises the question: I wonder what other directions it could have gone in those intermediate states? Is it possible to snapshot the state of an LLM (or a cluster of them) "in the middle of proving FLT" and then prompt it to go in a different direction with all that context?
- bigstrat2003 12d ago
  > Now we add an LLM to that list. No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.
  - bjourne 12d ago
    A meme free of charge for you, sir: https://www.reddit.com/r/singularity/comments/1jl5qfs/its_just_predicting_tokens_v2/ https://www.reddit.com/r/singularity/comments/1jl5qfs/its_ju...
- traes 12d ago
  25-50 seems like a pretty lowball estimate, I guess depending on your definition of "understand."
mswphd 12d ago
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-second-and-third-generation-proofs-of-the-classification-of-fin/217397#217397 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.