6 ms·
> no prior solutions found. This is no longer true, a prior solution has just been found[1], so the LLM proof has been moved to the Section 2 of Terence Tao's
by xeeeeeeeeeeenu 8mo ago
> no prior solutions found.
This is no longer true, a prior solution has just been found[1], so the LLM proof has been moved to the Section 2 of Terence Tao's wiki[2].
[1] - https://www.erdosproblems.com/forum/thread/281#post-3325 https://www.erdosproblems.com/forum/thread/281#post-3325
[2] - https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems#2-fully-ai-generated-solutions-to-problems-for-which-subsequent-literature-review-found-full-or-partial-solutions https://github.com/teorth/erdosproblems/wiki/AI-contribution...
- davidhs 8mo agoIt looks like these models work pretty well as natural language search engines and at connecting together dots of disparate things humans haven't done.
- pfdietz 8mo agoThey're finding them very effective at literature search, and at autoformalization of human-written proofs. Pretty soon, this is going to mean the entire historical math literature will be formalized (or, in some cases, found to be in error). Consider the implications of that for training theorem provers.
- mlpoknbji 8mo agoI think "pretty soon" is a serious overstatement. This does not take into account the difficulty in formalizing definitions and theorem statements. This cannot be done autonomously (or, it can, but there will be serious errors) since there is no way to formalize the "text to lean" process. What's more, there's almost surely going to turn out to be a large amount of human generated mathematics that's "basically" correct, in the sense that there exists a formal proof that morally fits the arc of the human proof, but there's informal/vague reasoning used (e.g. diagram arguments, etc) that are hard to really formalize, but an expert can use consistently without making a mistake. This will take a long time to formalize, and I expect will require a large amount of human and AI effort.
- pfdietz 8mo agoIt's all up for debate, but personally I feel you're being too pessimistic there. The advances being made are faster than I had expected. The area is one where success will build upon and accelerate success, so I expect the rate of advance to increase and continue increasing. This particular field seems ideal for AI, since verification enables identification of failure at all levels. If the definitions are wrong the theorems won't work and applications elsewhere won't work.
- p-e-w 8mo agoEvery time this topic comes up people compare the LLM to a search engine of some kind. But as far as we know, the proof it wrote is original. Tao himself noted that it’s very different from the other proof (which was only found now). That’s so far removed from a “search engine” that the term is essentially nonsense in this context.
- theptip 8mo agoHassabis put forth a nice taxonomy of innovation: interpolation, extrapolation, and paradigm shifts. AI is currently great at interpolation, and in some fields (like biology) there seems to be low-hanging fruit for this kind of connect-the-dots exercise. A human would still be considered smart for connecting these dots IMO. AI clearly struggles with extrapolation, at least if the new datum is fully outside the training set. And we will have AGI (if not ASI) if/when AI systems can reliably form new paradigms. It’s a high bar.
- davidhs 8mo agoMaybe if Terence Tao had memorized the entire Internet (and pretty much all media), then maybe he would find bits and pieces of the problem remind him of certain known solutions and be able to connect the dots himself. But, I don't know. I tend to view these (reasoning) LLMs as alien minds and my intuition of what is perhaps happening under the hood is not good. I just know that people have been using these LLMs as search engines (including Stephen Wolfram), browsing through what these LLMs perhaps know and have connected together.
- threethirtytwo 8mo ago[flagged]
- catoc 8mo agoI firmly believe @threethirtytwo’s reply was not produced by an LLM
- mkarliner 8mo agoregardless of if this text was written by an LLM or a human, it is still slop,with a human behind it just trying to wind people up . If there is a valid point to be made , it should be made, briefly.
- catoc 8mo agoIf the point was triggering a reply, the length and sarcasm certainly worked. I agree brevity is always preferred. Making a good point while keeping it brief is much harder than rambling on. But length is just a measure, quality determines if I keep reading. If a comment is too long, I won’t finish reading it. If I kept reading, it wasn’t too long.
- nurettin 8mo agoWhy not plan for a future where a lot of non-trivial tasks are automated instead of living on the edge with all this anxiety?
- threethirtytwo 8mo ago[flagged]
- 7777332215 8mo agoIf all of it is going away and you should deny reality, what does everything else you wrote even mean?
- 8mo ago
- nl 8mo agoInteresting that in Terrance Tao's words: "though the new proof is still rather different from the literature proof)" And even odder that the proof was by Erdos himself and yet he listed it as an open problem!
- TZubiri 8mo agoMaybe it was in the training set.
- magneticnorth 8mo agoI think that was Tao's point, that the new proof was not just read out of the training set.
- rzmmm 8mo agoThe model has multiple layers of mechanisms to prevent carbon copy output of the training data.
- TZubiri 8mo agoforgive the skepticism, but this translates directly to "we asked the model pretty please not to do it in the system prompt"
- ffsm8 8mo agoIt's mind boggling if you think about the fact they're essential "just" statistical models It really contextualizes the old wisdom of Pythagoras that everything can be represented as numbers / math is the ultimate truth
- GrowingSideways 8mo agoHow so? Truth is naturally an apriori concept; you don't need a chatbot to reach this conclusion.
- cubefox 8mo agoThis illustrates how unimportant this problem is. A prior solution did exist, but apparently nobody knew because people didn't really care about it. If progress can be had by simply searching for old solutions in the literature, then that's good evidence the supposed progress is imaginary. And this is not the first time this has happened with an Erdős problem. A lot of pure mathematics seems to consist in solving neat logic puzzles without any intrinsic importance. Recreational puzzles for very intelligent people. Or LLMs.
- MattGaiser 8mo agoThere is still enormous value in cleaning up the long tail of somewhat important stuff. One of the great benefits of Claude Code to me is that smaller issues no longer rot in backlogs, but can be at least attempted immediately.
- cubefox 8mo agoThe difference is that Claude Code actually solves practical problems, but pure (as opposed to applied) mathematics doesn't. Moreover, a lot of pure mathematics seems to be not just useless, but also without intrinsic epistemic value, unlike science. See https://news.ycombinator.com/item?id=46510353 https://news.ycombinator.com/item?id=46510353
- jstanley 8mo agoApplications for pure mathematics can't necessarily be known until the underlying mathematics is solved. Just because we can't imagine applications today doesn't mean there won't be applications in the future which depend on discoveries that are made today.
- cubefox 8mo agoWell, read the linked comment. The possible future applications of useless science can't be known either. I still argue that it has intrinsic value apart from that, unlike pure mathematics.