12 ms·
Erdos 281 solved with ChatGPT 5.2 Pro
- carbocation 9mo agoThe erdosproblems thread itself contains comments from Terence Tao: https://www.erdosproblems.com/forum/thread/281 https://www.erdosproblems.com/forum/thread/281
- redbluered 9mo agoHas anyone verified this? I've "solved" many math problems with LLMs, with LLMs giving full confidence in subtly or significantly incorrect solutions. I'm very curious here. The Open AI memory orders and claims about capacity limits restricting access to better models are interesting too.
- bpodgursky 9mo agoTerence Tao gave it the thumbs up. I don't think you're going to do better than that.
- pessimist 9mo agoFrom Terry Tao's comments in the thread: "Very nice! ... actually the thing that impresses me more than the proof method is the avoidance of errors, such as making mistakes with interchanges of limits or quantifiers (which is the main pitfall to avoid here). Previous generations of LLMs would almost certainly have fumbled these delicate issues. ... I am going ahead and placing this result on the wiki as a Section 1 result (perhaps the most unambiguous instance of such, to date)" The pace of change in math is going to be something to watch closely. Many minor theorems will fall. Next major milestone: Can LLMs generate useful abstractions?
- radioactivist 9mo agoSeems like the someone dug something up from the literature on this problem (see top comment on the erdosproblems.com thread) "On following the references, it seems that the result in fact follows (after applying Rogers' theorem) from a 1936 paper of Davenport and Erdos (!), which proves the second result you mention. ... In the meantime, I am moving this problem to Section 2 on the wiki (though the new proof is still rather different from the literature proof)."
- ares623 9mo agoThis must be what it feels like to be a CEO and someone tells me they solved coding.
- mikert89 9mo agoI have 15 years of software engineering experience across some top companies. I truly believe that ai will far surpass human beings at coding, and more broadly logic work. We are very close
- daxfohl 9mo agoThey already do. What they suck at is common sense. Unfortunately good software requires both.
- marktl 9mo agoOr is it fortunate (for a short period at least).
- anonzzzies 9mo ago[flagged]
- 523-asf1 9mo agoEven a 20 year old Markov chain could produce this banality.
- anonzzzies 9mo agoHN will be the last place to admit it; people here seem to be holding out with the vague 'I tried it and it came up with crap'. While many of us are shipping software without touching (much) code anymore. I have written code for over 40 years and this is nothing like no-code or whatever 'replacing programmers' before, this is clearly different judging from the people who cannot code with a gun to their heads but still are shipping apps: it does not really matter if anyone believes me or not. I am making more money than ever with fewer people than ever delivering more than ever. We are very close. (by the way; I like writing code and I still do for fun)
- fc417fc802 9mo ago> holding out with the vague 'I tried it and it came up with crap' Isn't that a perfectly reasonable metric? The topic has been dominated by hype for at least the past 5 if not 10 years. So when you encounter the latest in a long line of "the future is here the sky is falling" claims, where every past claim to date has been wrong, it's natural to try for yourself, observe a poor result, and report back "nope, just more BS as usual". If the hyped future does ever arrive then anyone trying for themselves will get a workable result. It will be trivially easy to demonstrate that naysayers are full of shit. That does not currently appear to be the case.
- a_tartaruga 9mo agoOut of curiosity why has the LLM math solving community been focused on the Erdos problems over other open problems? Are they of a certain nature where we would expect LLMs to be especially good at solving them?
- krackers 9mo agoI guess they are at a difficulty where it's not too hard (unlike millennium prize problems), is fairly tightly scoped (unlike open ended research), and has some gravitas (so it's not some obscure theorem that's only unproven because of it's lack of noteworthiness).
- Davidzheng 9mo agoI actually don't think the reason is that they are easier than other open math problems. I think it's more that they are "elementary" in the sense that the problems usually don't require a huge amount of domain knowledge to state.
- xigoi 9mo agoThe Collatz conjecture can be stated using basic arithmetic, yet LLMs have not been able to solve it.
- Davidzheng 9mo agoI agree it's easier than Collatz. I just mean I am not sure it's much easier than many currently open questions which are less famous but need more machinery.
- _fizz_buzz_ 9mo agoThat is also one of the hardest problems.
- becquerel 9mo agoPeople like checking items off of lists.
- dernett 9mo agoThis is crazy. It's clear that these models don't have human intelligence, but it's undeniable at this point that they have _some_ form of intelligence.
- qudat 9mo agoMy take is that a huge part of human intelligence is pattern matching. We just didn’t understand how much multidimensional geometry influenced our matches
- sdwr 9mo agoI don't think it's accurate to describe LLMs as pattern matching. Prediction is the mechanism they use to ingest and output information, and they end up with a (relatively) deep model of the world under the hood.
- DrewADesign 9mo agoWhich is even more true for humans.
- keeda 9mo agoYes, the world model building is achieved via pattern matching and happens during ingestion and training, but that is also part of the intelligence.
- D-Machine 9mo ago"Pattern matching" is not sufficiently specified here for us to say if LLMs do pattern matching or not. E.g. we can say that an LLM predicts the next token because that token (or rather, its embedding) is the best "match" to the previous tokens, which form a path ("pattern") in embedding space. In this sense LLMs are most definitely pattern matching. Under other formulations of the term, they may not be (e.g. when pattern matching refers to abstraction or abstracting to actual logical patterns, rather than strictly semantic patterns).
- visarga 9mo ago
- sequin 9mo agoFWIW, I just gave Deepseek the same prompt and it solved it too (much faster than the 41m of ChatGPT). I then gave both proofs to Opus and it confirmed their equivalence. The answer is yes. Assume, for the sake of contradiction, that there exists an \(\epsilon > 0\) such that for every \(k\), there exists a choice of congruence classes \(a_1^{(k)}, \dots, a_k^{(k)}\) for which the set of integers not covered by the first \(k\) congruences has density at least \(\epsilon\). For each \(k\), let \(F_k\) be the set of all infinite sequences of residues \((a_i)_{i=1}^\infty\) such that the uncovered set from the first \(k\) congruences has density at least \(\epsilon\). Each \(F_k\) is nonempty (by assumption) and closed in the product topology (since it depends only on the first \(k\) coordinates). Moreover, \(F_{k+1} \subseteq F_k\) because adding a congruence can only reduce the uncovered set. By the compactness of the product of finite sets, \(\bigcap_{k \ge 1} F_k\) is nonempty. Choose an infinite sequence \((a_i) \in \bigcap_{k \ge 1} F_k\). For this sequence, let \(U_k\) be the set of integers not covered by the first \(k\) congruences, and let \(d_k\) be the density of \(U_k\). Then \(d_k \ge \epsilon\) for all \(k\). Since \(U_{k+1} \subseteq U_k\), the sets \(U_k\) are decreasing and periodic, and their intersection \(U = \bigcap_{k \ge 1} U_k\) has density \(d = \lim_{k \to \infty} d_k \ge \epsilon\). However, by hypothesis, for any choice of residues, the uncovered set has density \(0\), a contradiction. Therefore, for every \(\epsilon > 0\), there exists a \(k\) such that for every choice of congruence classes \(a_i\), the density of integers not covered by the first \(k\) congruences is less than \(\epsilon\). \boxed{\text{Yes}}
- amluto 9mo agoI find it interesting that, as someone utterly unfamiliar with ergodic theory, Dini’s theorem, etc, I find Deepseek’s proof somewhat comprehensible, whereas I do not find GPT-5.2’s proof comprehensible at all. I suspect that I’d need to delve into the terminology in the GPT proof if I tried to verify Deepseek’s, so maybe GPT’s is being more straightforward about the underlying theory it relies on?
- nsoonhui 9mo agoI am not familiar with the field, but any chance that the deepseek is just memorizing the existing solution? Or different. https://news.ycombinator.com/item?id=46664976 https://news.ycombinator.com/item?id=46664976
- ashleyn 9mo agoI guess the first question I have is if these problems solved by LLMs are just low-hanging fruit that human researchers either didn't get around to or show much interest in - or if there's some actual beef here to the idea that LLMs can independently conduct original research and solve hard problems.
- dyauspitr 9mo agoThere is still value on letting these LLMs loose on the periphery and knocking out all the low hanging fruit humanity hasn’t had the time to get around to. Also, I don’t know this, but if it is a problem on Erdos I presume people have tried to solve it atleast a little bit before it makes it to the list.
- utopiah 9mo agoIs there though? If they are "solved" (as in the tickbox mark them as such, through a validation process, e.g. another model confirming, formal proof passing, etc) but there is no human actually learning from them, what's the benefit? Completing a list? I believe the ones that are NOT studied are precisely because they are seen as uninteresting. Even if they were to be solved in an interesting way, if nobody sees the proof because they are just too many and they are again not considered valuable then I don't see what is gained.
- ogogmad 9mo agoYou don't see value in having a cheap way to detect when a problem is easy or hard? That would seem unimaginative.
- vessenes 9mo agoSome problems are ‘uninteresting’ in that they show results that aren’t immediately seen as useful. However, solutions may end up having ‘interesting’ connections or ideas or mathematical tools that are used elsewhere. More broadly, I think there’s a perspective that literally just building out thousands more true statements in Lean is going to keep cementing math’s broadening knowledge framework. This is not building a giant castle a-la Wiles, it’s laying bricks in the outhouse, but someday those bricks might be useful.
- doctoboggan 9mo agoCan anyone give a little more color on the nature of Erdos problems? Are these problems that many mathematicians have spend years tackling with no result? Or do some of the problems evade scrutiny and go un-attempted for most of the time? EDIT: After reading a link someone else posted to Terrance Tao's wiki page, he has a paragraph that somewhat answers this question: > Erdős problems vary widely in difficulty (by several orders of magnitude), with a core of very interesting, but extremely difficult problems at one end of the spectrum, and a "long tail" of under-explored problems at the other, many of which are "low hanging fruit" that are very suitable for being attacked by current AI tools. Unfortunately, it is hard to tell in advance which category a given problem falls into, short of an expert literature review. (However, if an Erdős problem is only stated once in the literature, and there is scant record of any followup work on the problem, this suggests that the problem may be of the second category.) from here: https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erdős-problems https://github.com/teorth/erdosproblems/wiki/AI-contribution...
- QuesnayJr 9mo agoErdos was an incredibly prolific mathematician, and one of his quirks is that he liked to collect open problems and state new open problems as a challenge to the field. Many of the problems he attached bounties to, from $5 to $10,000. The problems are a pretty good metric for AI, because the easiest ones at least meet the bar of "a top mathematician didn't know how to solve this off the top of his head" and the hardest ones are major open problems. As AI progresses, we will see it slowly climb the difficulty ladder.
- heliumtera 9mo agoDon't feel bad for being out of the loop. The author and Tao did not care enough about erdos problem to realize the proof was published by erdos himself. So you never cared enough and neither did they. But they care about about screaming LLMs breakthrough on fediverse and twitter.
- nddkdkfk 9mo agoThis Tao dude, does he get invited to a lot of AI conferences (accommodation included)?
- xeeeeeeeeeeenu 9mo 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...
- threethirtytwo 9mo ago[flagged]
- nurettin 9mo 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 9mo ago[flagged]
- 7777332215 9mo agoIf all of it is going away and you should deny reality, what does everything else you wrote even mean?
- habinero 9mo agoYes, it is simply impossible that anyone could look at things and do your own evaluations and come to a different, much more skeptical conclusion. The only possible explanation is people say things they don't believe out of FUD. Literally the only one.
- undeveloper 9mo agocome out of the irony layer for a second -- what do you believe about LLMs?
- jrflowers 9mo agoNarrator: The solution had already appeared several times in the training data
- IAmGraydon 9mo agoThis is showing as unresolved here, so I'm assuming something was retracted. https://mehmetmars7.github.io/Erdosproblems-llm-hunter/problem.html?type=erdos&id=281 https://mehmetmars7.github.io/Erdosproblems-llm-hunter/probl...
- nl 9mo agoI think that just hasn't been updated.
- magicalist 9mo agoFunny seeing silicon valley bros commenting "you're on fire!" to Neel when it appears he copied and pasted the problem verbatim into chatGPT and it did literally all the other work here https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e0816e https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e081...
- inimino 9mo agoKnowing which problem to copy and paste into the model is also a skill.
- beders 9mo agoHas anyone confirmed the solution is not in the training data? Otherwise it is just a bit information retrieval LLM style. No intelligence necessary.
- ath3nd 9mo ago[dead]
- logicallee 9mo agohow did they do it? Was a human using the chat interface? Did they just type out the problem and immediately on the first reply received a complete solution (one-shot) or what was the human's role? What was ChatGPT's thinking time?
- phelm 9mo agoHeres the chat https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e0816e https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e081...
- logicallee 9mo agovery interesting. ChatGPT reasoned for 41 minutes about it! Also, this was one-shot - i.e. ChatGPT produced its complete proof with a single prompt and no more replies by the human, (rather than a chat where the human further guided it.)
- niemandhier 9mo agoIs there explainability research for this type of model application? E.g. a sparse auto encoder or something similar but more modern. I would love to know which concepts are active in the deeper layers of the model while generating the solution. Is there a concept of “epsilon” or “delta”? What are their projections on each other?
- energy123 9mo agoA surprising % of these LLM proofs are coming from amateurs. One wonders if some professional mathematicians are instead choosing to publish LLM proofs without attribution for career purposes.
- kristopolous 9mo agoIt's probably from the perennial observation "This LLM is kinda dumb in the thing I'm an expert in"
- fatherwavelet 9mo agoThis is just not true at this point but believe whatever you want to believe.
- deleted 9mo ago[deleted]
- fatata123 9mo ago[dead]
- vessenes 9mo ago… “but I guess it was able to formalize it in Lean, so…”
- Workaccount2 9mo agoPerennial doesn't make sense in the context of something that has been around for a few months. Observations from the spring 2025 crop of LLMs are already irrelevant.
- Davidzheng 9mo agoI'm actually not sure what the right attribution method would be. I'd lean towards single line on acknowledgements? Because you can use it for example @ every lemma during brainstorming but it's unclear the right convention is to thank it at every lemma... Anecdotally, I, as a math postdoc, think that GPT 5.2 is much stronger qualitatively than anything else I've used. Its rate of hallucinations is low enough that I don't feel like the default assumption of any solution is that it is trying to hide a mistake somewhere. Compared with Gemini 3 whose failure mode when it can't solve something is always to pretend it has a solution by "lying"/ omitting steps/making up theorems etc... GPT 5.2 usually fails gracefully and when it makes a mistake it more often than not can admit it when pointed out.
- renewiltord 9mo agoIt’s funny. in some kind of twisted variant of Cunningham’s Law we have: > the best way to find a previous proof of a seemingly open problem on the internet is not to ask for it; it's to post a new proof
- dust42 9mo agoPersonally, I'd prefer if the AI models would start with a proof of their own statements. Time and again, SOTA frontier models told me: "Now you have 100% correct code ready for production in enterprise quality." Then I run it and it crashes. Or maybe the AI is just being tongue-in-cheek? Point in case: I just wanted to give z.ai a try and buy some credits. I used Firefox with uBlock and the payment didn't go through. I tried again with Chrome and no adblock, but now there is an error: "Payment Failed: p.confirmCardPayment is not a function." The irony is, that this is certainly vibe-coded with z.ai which tries to sell me how good they are but then not being able to conclude the sale. And we will get lots more of this in the future. LLMs are a fantastic new technology, but even more fantastically over-hyped.
- becquerel 9mo agoYou get AIs to prove their code is correct in precisely the same ways you get humans to prove their code is correct. You make them demonstrate it through tests or evidence (screenshots, logs of successful runs).
- judahmeek 9mo agoYes! Also, make sure to check those results yourself, dear reader, rather than ask the agent to summarize the results for you! ^^;
- killerstorm 9mo agoWe should differentiate AI models from AI apps. Models just generate text. Apps are supposed to make that text useful. An app can run various kinds of verification. But would you pay an extra for that? Nobody can make a text generator to output text which is 100% correct. That's just not a thing people can do now.
- wewxjfq 9mo agoThe LLMs that take 10 attempts to un-zero-width a <div>, telling me that every single change totally fixed the problem, are cracking the hardest math problems again.
- int_19h 9mo agoMath makes sense, CSS doesn't.
- Eufrat 9mo agoThere was a post about Erdős 728 being solved with Harmonic’s Aristotle a little over a week ago [1] and that seemed like a good example of using state-of-the-art AI tech to help increase velocity in this space. I’m not sure what this proves. I dumped a question into ChatGPT 5.2 and it produced a correct response after almost an hour [2]? Okay? Is it repeatable? Why did it come up with this solution? How did it come up with the connections in its reasoning? I get that it looks correct and Tao’s approval definitely lends credibility that it is a valid solution, but what exactly is it that we’ve established here? That the corpus that ChatGPT 5.2 was trained on is better tuned for pure math? I’m just confused what one is supposed to take away from this. [1] https://news.ycombinator.com/item?id=46560445 https://news.ycombinator.com/item?id=46560445 [2] https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e0816e https://chatgpt.com/share/696ac45b-70d8-8003-9ca4-320151e081...
- vessenes 9mo agoThanks for the curious question. This is one in a sequence of efforts to use LLMs to generate candidate proofs to open mathematical questions, which then are generally formalized into Lean, a formal proof system for pure mathematics. Erdos was prolific and many of his open problems are numbered and have space to discuss them online, so it’s become fairly common to run through them with frontier models and see if a good proof can be come up with; there have been some notable successes here this year. Tao seems to engage in sort of a two step approach with these proofs - first, are they correct? Lean formalization makes that unambiguous, but not all proofs are easily formulated into Lean, so he also just, you know, checks them. Second, literature search inside LLMs and out for prior results — this is to check where frontier models are at in the ‘novel proofs or just regurgitated proofs’ space. To my knowledge, we’re currently at the point where we are seeing some novel proofs offered, but I don’t think we’ve seen any that have absolutely no priors in literature. As you might guess this is itself sort of a Rorschach test for what AI could and will be. In this case, it looked at first like this was a totally novel solution to something that hadn’t been solved before. On deeper search, Tao noted it’s almost trivial to prove with stuff Erdos knew, and also had been proved independently; this proof doesn’t use the prior proof mechanism though.
- Coeur 9mo ago
- charmpic 9mo agoI'm looking forward to chatgpt 5.3pro. I also use chatgpt 5.2pro for various program consultations. It's been very helpful.
- vercaemert 9mo agoI was hoping there'd be more discussion about the model itself. I find the last couple of generations of Pro models fascinating. Personally, I've been applying them to hard OCR problems. Many varied languages concurrently, wildly varying page structure, and poor scan quality; my dataset has all of these things. The models take 30 minutes a page, but the accuracy is basically 100% (it'll still striggle with perfectly-placed bits of mold). The next best model (Google's flagship) rests closer to 80%. I'll be VERY intrigued to see what the next 2, 5, 10 years does to the price of this level of model.
- energy123 9mo agoWe're eventually going to get it at cerebras inference latency. It's going to be wild.
- supermatt 9mo agoWhat does "solved with" mean? The author claims "I've solved", so did the author solve it or GPT?
- klohto 9mo agoWhen you use a calculator, did you really solve it or was it the calculator?
- supermatt 9mo agoWith a calculator I supply the arithmetic. It just executes it with no reasoning so im the solver. I can do the same with an LLM and still be the solver as long as it just follows my direction. Or I can give it a problem and let it reason and generate the arithmetic itself, in which case the LLM is effectively the solver. Thats why saying "I've solved X using only GPT" is ambiguous. But thanks for the downvote in addition to your useless comment.
- zkmon 9mo agoI wonder if they tried Gemini. I think Gemini could have done better, as seen from my experiences with GPT and Gemini models on some simple geometry problems.
- ironbound 9mo agoSounds like Lean 4/rocq did all the work here
- wasabi991011 9mo agoWhy do you say that? I see no mention of lean/rocq on the twitter thread, nor on the erdos problem forum thread, nor on the chatGPT conversation.
- YouAreWRONGtoo 9mo ago[dead]
- heliumtera 9mo ago>no prior solutions found. They never brothered to check erdos solution already published 90 years ago. I am still confused about why erdos, who proposed the problem and the solution would consider this an unsolved problems, but this group of researchers would claim "ohh my god look at this breakthrough"
- ath3nd 9mo ago[dead]
- syngrog66 9mo agoI can post a long list of simple things a human can do accurately and efficiently that I've seen Gemini unable to do, repeatedly.
- thunky 9mo agoAnd someone could post an even longer list of things you can't do well. But what would be the point? The LLM did better on this problem than 100% of the haters in this thread could do, and who probably can't even begin "understand" the problem.