AI just proved Erdos Problem #124
37 points
by nl
5 hours ago
| 6 comments
| twitter.com
| HN
demirbey05
19 minutes ago
[-]
This is response from mathematician: "This is quite something, congratulations to Boris and Aristotle!

On one hand, as the nice sketch provided below by tsaf confirms, the final proof is quite simple and elementary - indeed, if one was given this problem in a maths competition (so therefore expected a short simple solution existed) I'd guess that something like the below would be produced. On the other hand, if something like this worked, then surely the combined talents of Burr, Erdős, Graham, and Li would have spotted it.

Normally, this would make me suspicious of this short proof, in that there is overlooked subtlety. But (a) I can't see any and (b) the proof has been formalised in Lean, so clearly it just works!

Perhaps this shows what the real issue in the [BEGL96] conjecture is - namely the removal of 1 and the addition of the necessary gcd condition. (And perhaps at least some subset of the authors were aware of this argument for the easier version allowing 1, but this was overlooked later by Erdős in [Er97] and [Er97e], although if they were aware then one would hope they'd have included this in the paper as a remark.)

At the moment I'm minded to keep this as open, and add the gcd condition in the main statement, and note in the remarks that the easier (?) version allowing 1 and omitting the gcd condition, which was also asked independently by Erdős, has been solved."

The commentator is saying: "I can't believe this famous problem was solved so easily. I would have thought it was a fake proof, but the computer verified it. It turns out the solution works because it addresses a slightly different set of constraints (regarding the number 1) than what Erdős originally struggled with. (Generated by Gemini)

reply
ares623
2 hours ago
[-]
Here we go. Another tweet that can move hundreds of billions of dollars on the market and to justify a bail out. No accountability. Just the thrill to be the one to be able to say “first”.
reply
ComplexSystems
8 minutes ago
[-]
Are you kidding? This is an incredible result. Stuff like this is the most important stuff happening in AI right now. Automated theorem proving? It's not too far to say the entire singular point of the technology was to get us to this.
reply
bogdan
2 hours ago
[-]
Seriously, blame the investors.
reply
wasmainiac
1 hour ago
[-]
Nah, everyone is to blame here in bubble.
reply
adt
1 hour ago
[-]
Related, independent, and verified:

GPT-5 solved Erdős problem #848 (combinatorial number theory):

https://cdn.openai.com/pdf/4a25f921-e4e0-479a-9b38-5367b47e8...

https://lifearchitect.ai/asi/

reply
demirbey05
7 minutes ago
[-]
I read how GPT-5 contributed to proof. It is not fully solved by GPT-5 instead assisted. For more look here https://www.math.columbia.edu/~msawhney/Problem_848.pdf
reply
ares623
45 minutes ago
[-]
FTL? Seriously?
reply
menaerus
2 hours ago
[-]
This seems to be 2nd in row proof from the same author by using the AI models. First time it was the ChatGPT which wrote the formal Lean proof for Erdos Problem #340.

https://arxiv.org/html/2510.19804v1#Thmtheorem3

> In over a dozen papers, beginning in 1976 and spanning two decades, Paul Erdős repeatedly posed one of his “favourite” conjectures: every finite Sidon set can be extended to a finite perfect difference set. We establish that {1, 2, 4, 8, 13} is a counterexample to this conjecture.

reply
esperent
1 hour ago
[-]
More interesting discussion than on Twitter here:

https://www.erdosproblems.com/forum/thread/124#post-1892

reply
wasmainiac
1 hour ago
[-]
Ok… has this been verified? I see no publication or at least an announcement on Harmonics webpage. If this is a big deal, you think it would be a big deal, or is this just hype?
reply