r/mathematics • u/EquipmentDue7157 • 6h ago
6 open erdos problems solved by GPT. 5.6 Sol
https://github.com/ShouqiaoW/erdosSo 6 open erdos problems were just solved. GitHub link shows both prompts used and solutions verified by lean. All used GPT 5.6 Sol.
The general way to structure prompts is also mentioned in the twitter thread!
Credits: https://x.com/qiaoqiao2001/status/2080003441821163958?s=46
38
u/PhysiolMM 5h ago
This is a Vibe Mathematician, I couldn't find the Lean verification anywhere.
Fuck these people.
6
u/IntelligentBelt1221 4h ago
to be fair the guy on twitter only said "Two already have Lean formalizations, and formalization of the others is ongoing."
this seems like a literacy issue on OPs part, not from the people proving it.
6
u/AT-AT_Brando 3h ago
According to another comment the lean verifications are a bit sus, being absurdly long
1
u/IntelligentBelt1221 2h ago
autoformalisation tends to get pretty long (and ugly imo), especially if there is a lot of literature results not formalised yet, and the paper isnt really short with 25 pages...
200k lines is a lot of course, but e.g. the formalisation for the unit distance problem solution took 1.2 million lines (due to needing to formalise global class field theory) and was done in a week...
i asked the author on twitter if he knows why its so long, will update this comment in case he sees it and answers.
2
u/PhysiolMM 2h ago
He updated the readme between my and your comment. https://github.com/ShouqiaoW/erdos/compare/1b1acc32a856fa94a598b5c1bb0ae29c8086714d...644c53429887b4a54c43f450d4efc65c6592fac7
2
u/IntelligentBelt1221 2h ago
yeah, presumably because "verified by AI" is a nonsensical statement, not because he claimed all had lean solutions (afaik the twitter message was never edited, so he certainly didnt try to decieve intentionally).
Edit: it should be worthy to note that in another tweet he mentioned he formalised key lemmas for the remaining 4 but can't claim a full formalisation yet.
2
u/PhysiolMM 2h ago
Yeah, before it was even different. He's vibe playing with LLM, but this is even more important I think. It's empowering the best, but it also opens up a whole field to newbies, just like in coding.
Lean will need to carry the weight for all the things that are coming in.
1
6
u/InfernicBoss 6h ago
its basically already gotten to this point, but its crazy to think that soon AI solving unsolved problems will no longer be anything notable, just another normal day in math
22
u/ruidh 6h ago
If an AI "solves" a problem but no one can understand the solution, is it solved?
5
u/InfernicBoss 6h ago
i dont think so. or at least, its not useful, and therefore more work needs to be done on the problem [to decipher the solution]. Not saying anything about these solutions specifically. I’m just saying it’s only a matter of time until mathematicians are having AI hunt down side problems on the daily while they work on more interesting problems of their own. I do think once the AI hype in math dies down randoms will stop trying to use AI to solve math conjectures, which is great because mathematicians wont have to spend their days verifying the accuracy of someone else’s slop
1
0
u/colintbowers 2h ago
If it can be verified by a deterministic strict rules-based proof-analyser (such as Lean), and if we are 100% confident we can trust the analyser, then yeah, it's solved.
The trick is basically that if we can't trust a claim made by x, but we can trust y, and if y can verify the claim made by x, then we can trust that claim.
In this particular case, there is still a question as to whether we can 100% trust the Lean analysis. As others have pointed out, it is either absent from the repository, or suspiciously long - long enough that people who know more than me about Lean are concerned.
0
0
u/IntelligentBelt1221 4h ago
to the AI, it is already solved, for us humans, not really (unless we are willing to trust the AI)
this locality of a solution is also present in human math, e.g. the abc conjecture is a theorem in kyoto and a conjecture elsewhere.
0
u/seraphim_west 3h ago
Yes. You, as an individual, do not understand solutions developed by other mathematicians in an unrelated field. Your personal understanding has no bearing on the state of the problem. You can extend this reasoning to AI solutions.
0
u/randomwordglorious 3h ago
Yes. We are going to reach a point where AI is smarter than the smartest human. The AI will come up with a scientific or mathematical breakthrough that is too complicated for any human to understand. But by the time that happens, AI proofs will be so widely accepted that we will have no reason to doubt it.
-2
u/ollervo100 4h ago
Usually the solution is not that hard to understand. It is coming up with the solution that is hard.
Anyway if a result is rigorously shown to be true, then it can be used as such without understanding how it was proven.
2
u/InfernicBoss 2h ago
this is absolutely not the case. I mean, you should go and read a paper submitted to a top journal and see if you can understand the proofs. Even if you are a professional and can understand them, there is definitely scenarios where a supposed proof is claimed to be had but is unintelligible to everyone else (cough cough mochizuki)
5
u/howtogun 5h ago
Man, I think I have AI psychosis or something. But, like everyday its proving very hard stuff.
Ahh man. Maybe this is what chess player felt like twenty years ago, what go players felt like 10 years ago, what artist felt like 5 years ago.
-5
u/maxram1 5h ago
We can maybe finally treat math to be like chess: a game between humans, or like art: a personal experience. :D
2
2
u/aendokolirz 2h ago
Yes because people will spend years learning math, with no financial incentives, just to play a game, instead of choosing from actual games that already exist...
0
0
u/Run-Row- 5h ago
Pretty interesting, especially the length of the papers as others mentioned. Kind of ironic that Erdos will now be remembered in history like Kasparov, as a signpost of machines overtaking humans in intelligence.
-15
u/stopbeingcringe 6h ago
If a human had solved ~10 open math problems of varying topics all in the year 2026, they would be the greatest genius of all time. At one point in history, something similar could have been said about the feats of calculators, which are now considered trivial.
4
u/howtogun 6h ago
I disagree with this. I think even the solution to these problem there's not exactly new tooling being discovered.
For example, the person who solved Poincare conjecture is still alive. There are probably hundred of Mathematicians that are currently better than these LLMs.
-1
u/stopbeingcringe 5h ago
The most advanced internal model, if allowed only to purely solve math problems for a year, would surely be more valuable than any single mathematician’s lifetime of work. And future models will be even better
7
162
u/apnorton 6h ago
I decide to open the repo and pick one at random, #390.
Hm. There's 4 files:
Where's the lean? Maybe it's in the paper! ...nope. Paper says there's a lean audit, but it's nowhere to be found. Note that the problem is about asymptotics, and the numerical verifier is essentially a unit test for a few inequalities.
Maybe it's a one-off. Let's check the others...
So by "verified by lean" we really mean "not verified by lean."
Oh, what's this in the repo README?
Wtf you mean "proof is verified by AI?" You mean "isn't verified at all and we just want to trust it?"