10 ms·

AI just proved Erdos Problem #124

242 points by nl 11mo ago

https://twitter.com/vladtenev/status/1994922827208663383 https://twitter.com/vladtenev/status/1994922827208663383

ares623 11mo ago
[flagged]
- bogdan 11mo ago
  Seriously, blame the investors.
  - wasmainiac 11mo ago
    Nah, everyone is to blame here in bubble.
    - deleted 11mo ago
      [deleted]
- dang 11mo ago
  "Please don't post shallow dismissals, especially of other people's work. A good critical comment teaches us something." "Don't be curmudgeonly. Thoughtful criticism is fine, but please don't be rigidly or generically negative." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
menaerus 11mo 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 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.
- NooneAtAll3 11mo ago
  that one was vibe-coded Ai was given step-by-step already found proof, and asked "please rewrite in Lean" --- here Ai did the proof itself
- TacticalCoder 11mo ago
  [dead]
adt 11mo ago
Related, independent, and verified: GPT-5 solved Erdős problem #848 (combinatorial number theory): https://cdn.openai.com/pdf/4a25f921-e4e0-479a-9b38-5367b47e8fd0/early-science-acceleration-experiments-with-gpt-5.pdf https://cdn.openai.com/pdf/4a25f921-e4e0-479a-9b38-5367b47e8... https://lifearchitect.ai/asi/ https://lifearchitect.ai/asi/
- ares623 11mo ago
  FTL? Seriously?
  - mrguyorama 11mo ago
    It's utter horseshit. "New element" is partially completed, linking to a video of Microsoft claiming a new coolant fluid, oh and the link to the "paper" is a link to a blog post that is 90% advertising and at no point even pretends to claim there is a "new element" of some sort. One of his requirements is "Borders don't exist" like jeeze It's just lies. These people are all lies, or worse, are so utterly divorced from reality and don't even know what the words they say mean The person who runs that site claims to be an "ai expert", and leads with his "Doctor" title despite nobody being willing to tell you what he got his doctorate in, and spends all his time writing pop-"sci" slop. One brag point the instution that sells his speaking services points out is that his dissertation was adapted into a book about "Smart people are naturally smart and better than you" and brags about how it involved "Dr Rupert Sheldrake", the well known pseudo-scientist >He is a AI consultant whose 2021-2022 experiments with Leta AI and Aurora AI have been viewed over 5 million times. >Alan completed his Bachelor of Science (Computer Science, AI, and Psychology) at Edith Cowan University, 2004; studied Gifted Education at Flinders University, 2017; became a Fellow of the Institute of Coaching affiliated with Harvard Medical School, 2017; and received his doctorate from Emerson, 2021. Alan’s dissertation was adapted into a book featuring Dr Rupert Sheldrake, Connected: Intuition and Resonance in Smart People. >Alan was a major contributor to human intelligence research and practice. As chairman for Mensa International’s gifted families committee, Alan served two consecutive terms sharing best practice among 54 countries, and his work on gifted education was referenced in the Department of Education’s High Potential policy. Look at all that title inflation baby! Surely executive material! I mean just come on I can't believe people who fall for this trash are able to breathe Classic grifter trash.
wasmainiac 11mo 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?
- singularity2001 11mo ago
  verified by lean so 99.99% yes
  - cluckindan 11mo ago
    Lean verified a proof of a solution to a problem, but was it the same problem as Erdős problem #124? https://www.erdosproblems.com/forum/thread/124#post-1899 https://www.erdosproblems.com/forum/thread/124#post-1899
    - wasmainiac 11mo ago
      > My summary is that Aristotle solved "a" version of this problem (indeed, with an olympiad-style proof), but not "the" version. > I agree that the [BEGL96] problem is still open (for now!), and your plan to keep this problem open by changing the statement is reasonable. Alternatively, one could add another problem and link them. I have no preference. — BorisAlexeev There we go, so there is hype to some degree.
  - aaomidi 11mo ago
    Is there some good literature to read about lean? First time I’m hearing about it and it seems pretty cool.
    - anon291 11mo ago
      Anything in type theory. Lean is fundamentally a strongly typed dependently typed programming language. Start with Haskell and keep going.
esperent 11mo ago
More interesting discussion than on Twitter here: https://www.erdosproblems.com/forum/thread/124#post-1892 https://www.erdosproblems.com/forum/thread/124#post-1892
- dang 11mo ago
  Ok, we've changed the link to that from https://twitter.com/vladtenev/status/1994922827208663383 https://twitter.com/vladtenev/status/1994922827208663383, but I've included the latter in the toptext. Thanks!
demirbey05 11mo 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)
- aaomidi 11mo ago
  I think that person is the owner of the website discussing it too. He was cited https://the-decoder.com/leading-openai-researcher-announced-a-gpt-5-math-breakthrough-that-never-happened/ https://the-decoder.com/leading-openai-researcher-announced-... Where a while back OpenAI made a misleading claim about solving some of these problems.
- dang 11mo ago
  > Generated by Gemini Please don't post generated comments here. We want HN to be a place for humans writing in their own voice.
ComplexSystems 11mo 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.
- ares623 11mo ago
  This is me being snarky and ignorant, but if it solved one problem and it is automated what’s stopping it from solving all the others? That’s what’s ultimately being sold by the tweet right.
  - aeve890 11mo ago
    >This is me being snarky and ignorant, but if it solved one problem and it is automated what’s stopping it from solving all the others? Yeah that's the crux of the matter. How do AI did it? Using already existing math. If we need new math to prove Collatz, Goldbach or Riemman, LLMs are simply SOL. That's what's missing and hype boys always avoid to mention.
    - dwohnitmok 11mo ago
      > How do AI did it? Using already existing math. If we need new math to prove Collatz, Goldbach or Riemman, LLMs are simply SOL. An unproved theorem now proved is by definition new math. Will LLMs get you to Collatz, Goldbach, or Riemann? Unclear. But it's not like there's some magical, entirely unrelated to existing math, "new math" that was required to solve all the big conjectures of the past. They proceeded, as always, by proving new theorems one by one.
      - yorwba 11mo ago
        Yes, "new math" is neither magical nor unrelated to existing math, but that doesn't mean any new theorem or proof is automatically "new math." I think the term is usually reserved for the definition of a new kind of mathematical object, about which you prove theorems relating it to existing math, which then allows you to construct qualitatively new proofs by transforming statements into the language of your new kind of object and back. I think eventually LLMs will also be used as part of systems that come up with new, broadly useful definitions, but we're not there yet.
BanditDefender 11mo ago
"Mathematicial superintelligence" is so obnoxious. Why exactly do they think it is called an Erdős problem when Erdős didn't find the solution? Because Erdős discovered the real mathematics: the conjecture! These people treat math research as if it is a math homework assignment. There needs to be an honest discussion about what the LLM is doing here. When you bang your head against a math problem you blindly try a bunch of dumb ideas that don't actually work. It wastes a lot of paper. The LLM automates a lot of that. It is actually pretty cool that modern AI can help speed this up and waste less paper. It is very similar to how classical AI (Symbolica) sped up math research and wasted less paper. But we need to have an honest discussion about how we are using the computer as a tool. Instead malicious idiots like Vlad Tenev are making confident predictions about mathematical superintelligence. So depressing.
consumer451 11mo ago
For reference, this is from: https://harmonic.fun/ https://harmonic.fun/ related article: > Is Math the Path to Chatbots That Don’t Make Stuff Up? https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html https://www.nytimes.com/2024/09/23/technology/ai-chatbots-ch...
- anon291 11mo ago
  Chat bots will necessarily 'make stuff up' (i.e. get things wrong) due to the random sampling and the law of big numbers. I don't understand why I have to keep repeating this on a forum filled with technical and numerically inclined people.
  - consumer451 11mo ago
    I was not shilling for them, just trying to give context to a Twitter post, after I clicked through and learned about the company.
mmmmbbbhb 11mo ago
Meanwhile I have to use ai just to understand the problem statement.
- lolive 11mo ago
  Which makes you the top 1% power users of AI. [the other 99% asking for the breast size of whoever starlette appeared on TV]
  - sebastiennight 11mo ago
    That's not what we mean when we're asking for "the release of bigger models"
    - Dilettante_ 11mo ago
      200DD parameters
      - lolive 11mo ago
        Bigger is not always better. [Gemini told me that yesterday, during my daily psychotherapy]
deleted 11mo ago
[deleted]
sheepscreek 11mo ago
It’s crazy that the empathetic AI I sometimes share my life’s mundane problems with wrote this. It understands such high level maths and speaks in a lexicon with words I can’t even pronounce. Incredible versatility. If this isn’t AGI (or even super intelligence) then what is? Sure it suffers from amnesia and cannot get basic things right sometimes, but one is a design limitation that can be overcome and the other a possible problem caused by training (we’re discovering that overt focus during training on adherence to prompt somewhat lobotomizes their general competence).
- vrighter 11mo ago
  As for the first: Everything points towards the problem NOT being able to be overcome with current architectures. For the 2nd: We are completely 100% sure this cannot be solved. This is not a training issue. This is the case for any statistical machine. No amount of training can ever solve this.
- encyclopedism 11mo ago
  This is a poor take on what LLM's actually are. They don't understand in any real sense. If you had enough paper and ink and the patience to go through it all you could take all the training data and manually step through and train the same model. Then once you have trained the model you could use more pen and paper to step through the correct prompts to arrive at the answer. All of this would be a completely mechanical process.
magicalist 11mo ago
The overhyped tweet from the robinhood guy raising money for his AI startup is nicely brought into better perspective by Thomas Bloom (including that #124 is not from the cited paper, "Complete sequences of sets of integer powers "/BEGL96): > This is a nice solution, and impressive to be found by AI, although the proof is (in hindsight) very simple, and the surprising thing is that Erdos missed it. But there is definitely precedent for Erdos missing easy solutions! > Also this is not the problem as posed in that paper > That paper asks a harder version of this problem. The problem which has been solved was asked by Erdos in a couple of later papers. > One also needs to be careful about saying things like 'open for 30 years'. This does not mean it has resisted 30 years of efforts to solve it! Many Erdos problems (including this one) have just been forgotten about it, and nobody has seriously tried to solve it.[1] And, indeed, Boris Alexeev (who ran the problem) agrees: > My summary is that Aristotle solved "a" version of this problem (indeed, with an olympiad-style proof), but not "the" version. > I agree that the [BEGL96] problem is still open (for now!), and your plan to keep this problem open by changing the statement is reasonable. Alternatively, one could add another problem and link them. I have no preference.[2] Not to rain on the parade out of spite, it's just that this is neat, but not like, unusually neat compared to the last few months. [1] https://twitter.com/thomasfbloom/status/1995083348201586965 https://twitter.com/thomasfbloom/status/1995083348201586965 [2] https://www.erdosproblems.com/forum/thread/124#post-1899 https://www.erdosproblems.com/forum/thread/124#post-1899
- NooneAtAll3 11mo ago
  I was so happy for this result until I saw your mention of robinhood hype :/
- NooneAtAll3 11mo ago
  reading the original paper and the lean statement that got proven, it's kinda fascinating what exactly is considered interesting and hard in this problem roughly, what lean theorem (and statement on the website) asks is this: take some numbers t_i, for each of them form all the powers t_i^j, then combine all into multiset T. Barring some necessary conditions, prove that you can take subset of T to sum to any number you want what Erdosh problem in the paper asks is to add one more step - arbitrarily cut off beginnings of t_i^j power sequences before merging. Erdosh-and-co conjectured that only finite amount of subset sums stop being possible "subsets sum to any number" is an easy condition to check (that's why "olympiad level" gets mentioned in the discussion) - and it's the "arbitrarily cut off" that's the part that og question is all about, while "only finite amount disappear" is hard to grasp formulaically so... overhyped yes, not actually erdos problem proven yes, usual math olympiad level problems are solvable by current level of Ai as was shown by this year's IMO - also yes (just don't get caught by https://en.wikipedia.org/wiki/AI_effect https://en.wikipedia.org/wiki/AI_effect on the backlash since olympiads are haaard! really!)
WhyOhWhyQ 11mo ago
I predict the way AI will be useful in science from the perspective of mathematics is by figuring out combinatorially complex solutions to problems that would otherwise not be interesting to (or far too complex to be comprehended by) humans. With such capabilities it could be imagined then that the AI will be useful for designing super materials, or doing fancy things with biology / medicine, and generally finding useful patterns in complex systems.
- estebarb 11mo ago
  However, they at most would be the heuristic function of a search mechanism. A good heuristic, but heuristic at most. For search we need to identify when to abandon a path and which other entry point is promising. I'm not sure our current techniques are good for this kind of problems.
- bluecalm 11mo ago
  I think it will be even more helpful to know a simple proof doesn't exist because AI has tried for long enough and didn't find it. Once people know there is no easy proof of say Collatz or Twin Primes Conjencture those will not be as alluring to waste your time on.
- Someone 11mo ago
  But abstract mathematics doesn’t care about solutions to problems; it cares about understanding problem spaces. I do not think current AI helps with that. Problems like the one discussed also aren’t interesting to applied mathematicians, either, because of lack of applications. But yes, if this kind of AI produces new materials, solves diseases, etc. they will be very useful. We wouldn’t care whether they arrived at those solutions through valid reasoning, though. A sloppy AI that has better ‘guesses/intuitions’ than humans or that can guess and check ‘guesses/intuitions' for correctness faster would be very useful.
  - adastra22 11mo ago
    And engineers don’t care about abstract mathematics: we care about math that solves problems. Being able to solve more problems with less human-years of effort is a big win.
newmana 11mo ago
"Recently, yet another category of low-hanging fruit has been identified as within reach of automated tools: problems which, due to a technical flaw in their description, are unexpectedly easy to resolve. Specifically, problem #124 https://www.erdosproblems.com/124 https://www.erdosproblems.com/124 was a problem that was stated in three separate papers of Erdos, but in two of them he omitted a key hypothesis which made the problem a consequence of a known result (Brown's criterion). However, this fact was not noticed until Boris Alexeev applied the Aristotle tool to this problem, which autonomously located (and formalized in Lean) a solution to this weaker version of the problem within hours." https://mathstodon.xyz/@tao/115639984077620023 https://mathstodon.xyz/@tao/115639984077620023
- adastra22 11mo ago
  That doesn’t seem very fair. The problem was stated, and remained unsolved for all this time. You can’t take away that accomplishment just because the solution seems easy in hindsight.
  - zozbot234 11mo ago
    It's technically true that this version of the problem was "low-hanging fruit", so that's an entirely fair assessment. Systematically spotting low-hanging fruit that others had missed is an accomplishment, but it's quite different from solving a genuinely hard problem and we shouldn't conflate the two.
    - adastra22 11mo ago
      My point is stronger than that. Some things only appear low hanging fruit in hindsight. My own field of physics is full of examples. Saying “oh that should’ve been easy” is wrong more often than it is right.
      - zozbot234 11mo ago
        Sure, but unless all solvable problems can be said to "appear as low-hanging fruit in hindsight" this doesn't detract from Tao's assessment in any way. Solving a genuinely complex problem is a different matter than spotting simpler solutions that others had missed. In this case, the solution might have been missed before simply because the difference between the "easy" and "hard" formulations of the problem wasn't quite clear, including perhaps to Erdős, prior to it being restated (manually) as a Lean goal to be solved. So this is a success story for formalization as much as AI.
vatsachak 11mo ago
I know the problem the AI solved wasn't that hard but one should consider math toast within the next 10-15 years. Software engineering is more subtle since you actually care about the performance and semantics of a program. Unless you get really good at program specification, it would be difficult to fully automate. But with math the only thing you care about is whether the moves you made were right.
- emil-lp 11mo ago
  > one should consider math toast within the next 10-15 years. I keep a list of ridiculously failed predictions, and this goes into it. Can I ask you to be more concrete? What does "math is toast" mean to you?
  - n4r9 11mo ago
    I'd like to see some other instances from your list.
  - vatsachak 11mo ago
    In the sense that in 15 years my bet is that an AI system can solve my thesis problem for under 100$ https://ems.press/journals/jems/articles/14298293 https://ems.press/journals/jems/articles/14298293
    - emil-lp 11mo ago
      Math is toast if a computerized system can solve a problem you personally failed to solve during your PhD? Computers have proved stuff people couldn't since at least 1976 when Appel and Haken proved the 4-color theorem.
      - vatsachak 11mo ago
        The paper I linked is the problem I solved for my thesis, which was published in JEMS (upper echelon journal). I spent 8 hours a day for one and a half years working on it. 75% of mathematicians don't have a theorem that good, but the Terry Taos of the world get a theorem like that every year. My claim is that in 15 years an AI system will be able to prove it from first principles for under 100 dollars. That would render us normal mathematicians toast.
harshitaneja 11mo ago
The amount of goal post shifting is so amusing to see. Yes, sure this was probably not an "important" or a particularly "challenging" problem which had been open for a while. Sure, maybe it remained open because it didn't get enough eyeballs from the right people to care about spending time on it. Yes, there is too much overhyping and we are all tired of it somewhat. I still think if someone 10 years ago told me we would get "AI" to a stage where it can solve olympiad level problems and getting gold medals in IMO on top of doing so with input not in a very structured input but rather our complex, messy human natural language and being able to do so while interpreting, to various degrees of meaning what interpreting means, image and video data and doing so in almost real time I would have called you nuts and this thing in such a duration sci-fi. So some part of me feels crazy how quickly we have normalized to this new reality. A reality where we are talking about if the problem solved by the automated model using formal verification was too easy. Don't get me wrong, I am not saying any of this means we get AGI or something or even if we continue to see improvements. We can still appreciate things. It doesn't need to be a binary. What a time to be alive!
- Davidzheng 11mo ago
  Yeah, I agree. As a mathematician it's easy to say that it's not a super hard proof. But then again, the first proofs found by running AI on a large bucket of open problems was always going to be some easy proofs on a not-very-worked-on problem. The fact that no one did it before them definitely shows real progress being made. When you're an expert, it's hard to lose track of the fact that things that you consider trivial vs very hard may be in fact a very small distance in the grand scheme of things (rel to entities of different oom strengths)
- magicalist 11mo ago
  > The amount of goal post shifting is so amusing to see Can you be specific about the goal posts being shifted? Like the specific comments you're referring to here. Maybe I'm just falling for the bait, but non specific claims like this seem designed just to annoy while having nothing specific to converse about. I got to the end of your comment and counting all the claims you discounted, the only goal post I see left is that people aren't using a sufficiently excited tone while sifting fact from hype? A lot of us follow this work pretty closely and don't feel the need to start every post with "there is no need for excitement to abate, still exciting! but...". > I am not saying any of this means we get AGI or something or even if we continue to see improvements. We can still appreciate things. It doesn't need to be a binary. You'll note, however, that the hype guys happily include statements like "Vibe proving is here" in their posts with no nuance, all binary. Why not call them out?
kelseyfrog 11mo ago
An Erdos problem is great, but all major LLMs still score 0 out of 7 on all Millenium Prize Problems[1]. I, and I'm sure other like me, won't consider it "true" AI until AI saturate the MillenniumPrizeProblemBench. 1. https://www.claymath.org/millennium-problems/ https://www.claymath.org/millennium-problems/ 1.
- jfengel 11mo ago
  That's interesting, because what I'm looking for from AI is the opposite. Rather than looking to do something humans find hard, I'm more interested in the problems that humans find easy, like driving a car or counting the number of "r"s in a word. Having it go beyond that to do things that we can't do would be a nice bonus. But given the way AI has been going, I'd say there's a decent chance that it solves a Millennium Prize problem before it solves driving.

242 points by nl 11mo ago

https://twitter.com/vladtenev/status/1994922827208663383 https://twitter.com/vladtenev/status/1994922827208663383

ares623 11mo ago

[flagged]

bogdan 11mo ago
Seriously, blame the investors.
- wasmainiac 11mo ago
  Nah, everyone is to blame here in bubble.
  - deleted 11mo ago
    [deleted]
dang 11mo ago
"Please don't post shallow dismissals, especially of other people's work. A good critical comment teaches us something." "Don't be curmudgeonly. Thoughtful criticism is fine, but please don't be rigidly or generically negative." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html

menaerus 11mo 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 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.

NooneAtAll3 11mo ago
that one was vibe-coded Ai was given step-by-step already found proof, and asked "please rewrite in Lean" --- here Ai did the proof itself
TacticalCoder 11mo ago
[dead]

adt 11mo ago

Related, independent, and verified: GPT-5 solved Erdős problem #848 (combinatorial number theory): https://cdn.openai.com/pdf/4a25f921-e4e0-479a-9b38-5367b47e8fd0/early-science-acceleration-experiments-with-gpt-5.pdf https://cdn.openai.com/pdf/4a25f921-e4e0-479a-9b38-5367b47e8... https://lifearchitect.ai/asi/ https://lifearchitect.ai/asi/

ares623 11mo ago
FTL? Seriously?
- mrguyorama 11mo ago
  It's utter horseshit. "New element" is partially completed, linking to a video of Microsoft claiming a new coolant fluid, oh and the link to the "paper" is a link to a blog post that is 90% advertising and at no point even pretends to claim there is a "new element" of some sort. One of his requirements is "Borders don't exist" like jeeze It's just lies. These people are all lies, or worse, are so utterly divorced from reality and don't even know what the words they say mean The person who runs that site claims to be an "ai expert", and leads with his "Doctor" title despite nobody being willing to tell you what he got his doctorate in, and spends all his time writing pop-"sci" slop. One brag point the instution that sells his speaking services points out is that his dissertation was adapted into a book about "Smart people are naturally smart and better than you" and brags about how it involved "Dr Rupert Sheldrake", the well known pseudo-scientist >He is a AI consultant whose 2021-2022 experiments with Leta AI and Aurora AI have been viewed over 5 million times. >Alan completed his Bachelor of Science (Computer Science, AI, and Psychology) at Edith Cowan University, 2004; studied Gifted Education at Flinders University, 2017; became a Fellow of the Institute of Coaching affiliated with Harvard Medical School, 2017; and received his doctorate from Emerson, 2021. Alan’s dissertation was adapted into a book featuring Dr Rupert Sheldrake, Connected: Intuition and Resonance in Smart People. >Alan was a major contributor to human intelligence research and practice. As chairman for Mensa International’s gifted families committee, Alan served two consecutive terms sharing best practice among 54 countries, and his work on gifted education was referenced in the Department of Education’s High Potential policy. Look at all that title inflation baby! Surely executive material! I mean just come on I can't believe people who fall for this trash are able to breathe Classic grifter trash.

wasmainiac 11mo 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?

singularity2001 11mo ago
verified by lean so 99.99% yes
- cluckindan 11mo ago
  Lean verified a proof of a solution to a problem, but was it the same problem as Erdős problem #124? https://www.erdosproblems.com/forum/thread/124#post-1899 https://www.erdosproblems.com/forum/thread/124#post-1899
  - wasmainiac 11mo ago
    > My summary is that Aristotle solved "a" version of this problem (indeed, with an olympiad-style proof), but not "the" version. > I agree that the [BEGL96] problem is still open (for now!), and your plan to keep this problem open by changing the statement is reasonable. Alternatively, one could add another problem and link them. I have no preference. — BorisAlexeev There we go, so there is hype to some degree.
- aaomidi 11mo ago
  Is there some good literature to read about lean? First time I’m hearing about it and it seems pretty cool.
  - anon291 11mo ago
    Anything in type theory. Lean is fundamentally a strongly typed dependently typed programming language. Start with Haskell and keep going.

esperent 11mo ago

More interesting discussion than on Twitter here: https://www.erdosproblems.com/forum/thread/124#post-1892 https://www.erdosproblems.com/forum/thread/124#post-1892

dang 11mo ago
Ok, we've changed the link to that from https://twitter.com/vladtenev/status/1994922827208663383 https://twitter.com/vladtenev/status/1994922827208663383, but I've included the latter in the toptext. Thanks!

demirbey05 11mo 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)

aaomidi 11mo ago
I think that person is the owner of the website discussing it too. He was cited https://the-decoder.com/leading-openai-researcher-announced-a-gpt-5-math-breakthrough-that-never-happened/ https://the-decoder.com/leading-openai-researcher-announced-... Where a while back OpenAI made a misleading claim about solving some of these problems.
dang 11mo ago
> Generated by Gemini Please don't post generated comments here. We want HN to be a place for humans writing in their own voice.

ComplexSystems 11mo 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.

ares623 11mo ago
This is me being snarky and ignorant, but if it solved one problem and it is automated what’s stopping it from solving all the others? That’s what’s ultimately being sold by the tweet right.
- aeve890 11mo ago
  >This is me being snarky and ignorant, but if it solved one problem and it is automated what’s stopping it from solving all the others? Yeah that's the crux of the matter. How do AI did it? Using already existing math. If we need new math to prove Collatz, Goldbach or Riemman, LLMs are simply SOL. That's what's missing and hype boys always avoid to mention.
  - dwohnitmok 11mo ago
    > How do AI did it? Using already existing math. If we need new math to prove Collatz, Goldbach or Riemman, LLMs are simply SOL. An unproved theorem now proved is by definition new math. Will LLMs get you to Collatz, Goldbach, or Riemann? Unclear. But it's not like there's some magical, entirely unrelated to existing math, "new math" that was required to solve all the big conjectures of the past. They proceeded, as always, by proving new theorems one by one.
    - yorwba 11mo ago
      Yes, "new math" is neither magical nor unrelated to existing math, but that doesn't mean any new theorem or proof is automatically "new math." I think the term is usually reserved for the definition of a new kind of mathematical object, about which you prove theorems relating it to existing math, which then allows you to construct qualitatively new proofs by transforming statements into the language of your new kind of object and back. I think eventually LLMs will also be used as part of systems that come up with new, broadly useful definitions, but we're not there yet.

BanditDefender 11mo ago

"Mathematicial superintelligence" is so obnoxious. Why exactly do they think it is called an Erdős problem when Erdős didn't find the solution? Because Erdős discovered the real mathematics: the conjecture! These people treat math research as if it is a math homework assignment. There needs to be an honest discussion about what the LLM is doing here. When you bang your head against a math problem you blindly try a bunch of dumb ideas that don't actually work. It wastes a lot of paper. The LLM automates a lot of that. It is actually pretty cool that modern AI can help speed this up and waste less paper. It is very similar to how classical AI (Symbolica) sped up math research and wasted less paper. But we need to have an honest discussion about how we are using the computer as a tool. Instead malicious idiots like Vlad Tenev are making confident predictions about mathematical superintelligence. So depressing.

consumer451 11mo ago

For reference, this is from: https://harmonic.fun/ https://harmonic.fun/ related article: > Is Math the Path to Chatbots That Don’t Make Stuff Up? https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html https://www.nytimes.com/2024/09/23/technology/ai-chatbots-ch...

anon291 11mo ago
Chat bots will necessarily 'make stuff up' (i.e. get things wrong) due to the random sampling and the law of big numbers. I don't understand why I have to keep repeating this on a forum filled with technical and numerically inclined people.
- consumer451 11mo ago
  I was not shilling for them, just trying to give context to a Twitter post, after I clicked through and learned about the company.

mmmmbbbhb 11mo ago

Meanwhile I have to use ai just to understand the problem statement.

lolive 11mo ago
Which makes you the top 1% power users of AI. [the other 99% asking for the breast size of whoever starlette appeared on TV]
- sebastiennight 11mo ago
  That's not what we mean when we're asking for "the release of bigger models"
  - Dilettante_ 11mo ago
    200DD parameters
    - lolive 11mo ago
      Bigger is not always better. [Gemini told me that yesterday, during my daily psychotherapy]

deleted 11mo ago

[deleted]

sheepscreek 11mo ago

It’s crazy that the empathetic AI I sometimes share my life’s mundane problems with wrote this. It understands such high level maths and speaks in a lexicon with words I can’t even pronounce. Incredible versatility. If this isn’t AGI (or even super intelligence) then what is? Sure it suffers from amnesia and cannot get basic things right sometimes, but one is a design limitation that can be overcome and the other a possible problem caused by training (we’re discovering that overt focus during training on adherence to prompt somewhat lobotomizes their general competence).

vrighter 11mo ago
As for the first: Everything points towards the problem NOT being able to be overcome with current architectures. For the 2nd: We are completely 100% sure this cannot be solved. This is not a training issue. This is the case for any statistical machine. No amount of training can ever solve this.
encyclopedism 11mo ago
This is a poor take on what LLM's actually are. They don't understand in any real sense. If you had enough paper and ink and the patience to go through it all you could take all the training data and manually step through and train the same model. Then once you have trained the model you could use more pen and paper to step through the correct prompts to arrive at the answer. All of this would be a completely mechanical process.

magicalist 11mo ago

The overhyped tweet from the robinhood guy raising money for his AI startup is nicely brought into better perspective by Thomas Bloom (including that #124 is not from the cited paper, "Complete sequences of sets of integer powers "/BEGL96): > This is a nice solution, and impressive to be found by AI, although the proof is (in hindsight) very simple, and the surprising thing is that Erdos missed it. But there is definitely precedent for Erdos missing easy solutions! > Also this is not the problem as posed in that paper > That paper asks a harder version of this problem. The problem which has been solved was asked by Erdos in a couple of later papers. > One also needs to be careful about saying things like 'open for 30 years'. This does not mean it has resisted 30 years of efforts to solve it! Many Erdos problems (including this one) have just been forgotten about it, and nobody has seriously tried to solve it.[1] And, indeed, Boris Alexeev (who ran the problem) agrees: > My summary is that Aristotle solved "a" version of this problem (indeed, with an olympiad-style proof), but not "the" version. > I agree that the [BEGL96] problem is still open (for now!), and your plan to keep this problem open by changing the statement is reasonable. Alternatively, one could add another problem and link them. I have no preference.[2] Not to rain on the parade out of spite, it's just that this is neat, but not like, unusually neat compared to the last few months. [1] https://twitter.com/thomasfbloom/status/1995083348201586965 https://twitter.com/thomasfbloom/status/1995083348201586965 [2] https://www.erdosproblems.com/forum/thread/124#post-1899 https://www.erdosproblems.com/forum/thread/124#post-1899

NooneAtAll3 11mo ago
I was so happy for this result until I saw your mention of robinhood hype :/
NooneAtAll3 11mo ago
reading the original paper and the lean statement that got proven, it's kinda fascinating what exactly is considered interesting and hard in this problem roughly, what lean theorem (and statement on the website) asks is this: take some numbers t_i, for each of them form all the powers t_i^j, then combine all into multiset T. Barring some necessary conditions, prove that you can take subset of T to sum to any number you want what Erdosh problem in the paper asks is to add one more step - arbitrarily cut off beginnings of t_i^j power sequences before merging. Erdosh-and-co conjectured that only finite amount of subset sums stop being possible "subsets sum to any number" is an easy condition to check (that's why "olympiad level" gets mentioned in the discussion) - and it's the "arbitrarily cut off" that's the part that og question is all about, while "only finite amount disappear" is hard to grasp formulaically so... overhyped yes, not actually erdos problem proven yes, usual math olympiad level problems are solvable by current level of Ai as was shown by this year's IMO - also yes (just don't get caught by https://en.wikipedia.org/wiki/AI_effect https://en.wikipedia.org/wiki/AI_effect on the backlash since olympiads are haaard! really!)

WhyOhWhyQ 11mo ago

I predict the way AI will be useful in science from the perspective of mathematics is by figuring out combinatorially complex solutions to problems that would otherwise not be interesting to (or far too complex to be comprehended by) humans. With such capabilities it could be imagined then that the AI will be useful for designing super materials, or doing fancy things with biology / medicine, and generally finding useful patterns in complex systems.

estebarb 11mo ago
However, they at most would be the heuristic function of a search mechanism. A good heuristic, but heuristic at most. For search we need to identify when to abandon a path and which other entry point is promising. I'm not sure our current techniques are good for this kind of problems.
bluecalm 11mo ago
I think it will be even more helpful to know a simple proof doesn't exist because AI has tried for long enough and didn't find it. Once people know there is no easy proof of say Collatz or Twin Primes Conjencture those will not be as alluring to waste your time on.
Someone 11mo ago
But abstract mathematics doesn’t care about solutions to problems; it cares about understanding problem spaces. I do not think current AI helps with that. Problems like the one discussed also aren’t interesting to applied mathematicians, either, because of lack of applications. But yes, if this kind of AI produces new materials, solves diseases, etc. they will be very useful. We wouldn’t care whether they arrived at those solutions through valid reasoning, though. A sloppy AI that has better ‘guesses/intuitions’ than humans or that can guess and check ‘guesses/intuitions' for correctness faster would be very useful.
- adastra22 11mo ago
  And engineers don’t care about abstract mathematics: we care about math that solves problems. Being able to solve more problems with less human-years of effort is a big win.

newmana 11mo ago

"Recently, yet another category of low-hanging fruit has been identified as within reach of automated tools: problems which, due to a technical flaw in their description, are unexpectedly easy to resolve. Specifically, problem #124 https://www.erdosproblems.com/124 https://www.erdosproblems.com/124 was a problem that was stated in three separate papers of Erdos, but in two of them he omitted a key hypothesis which made the problem a consequence of a known result (Brown's criterion). However, this fact was not noticed until Boris Alexeev applied the Aristotle tool to this problem, which autonomously located (and formalized in Lean) a solution to this weaker version of the problem within hours." https://mathstodon.xyz/@tao/115639984077620023 https://mathstodon.xyz/@tao/115639984077620023

adastra22 11mo ago
That doesn’t seem very fair. The problem was stated, and remained unsolved for all this time. You can’t take away that accomplishment just because the solution seems easy in hindsight.
- zozbot234 11mo ago
  It's technically true that this version of the problem was "low-hanging fruit", so that's an entirely fair assessment. Systematically spotting low-hanging fruit that others had missed is an accomplishment, but it's quite different from solving a genuinely hard problem and we shouldn't conflate the two.
  - adastra22 11mo ago
    My point is stronger than that. Some things only appear low hanging fruit in hindsight. My own field of physics is full of examples. Saying “oh that should’ve been easy” is wrong more often than it is right.
    - zozbot234 11mo ago
      Sure, but unless all solvable problems can be said to "appear as low-hanging fruit in hindsight" this doesn't detract from Tao's assessment in any way. Solving a genuinely complex problem is a different matter than spotting simpler solutions that others had missed. In this case, the solution might have been missed before simply because the difference between the "easy" and "hard" formulations of the problem wasn't quite clear, including perhaps to Erdős, prior to it being restated (manually) as a Lean goal to be solved. So this is a success story for formalization as much as AI.

vatsachak 11mo ago

I know the problem the AI solved wasn't that hard but one should consider math toast within the next 10-15 years. Software engineering is more subtle since you actually care about the performance and semantics of a program. Unless you get really good at program specification, it would be difficult to fully automate. But with math the only thing you care about is whether the moves you made were right.

emil-lp 11mo ago
> one should consider math toast within the next 10-15 years. I keep a list of ridiculously failed predictions, and this goes into it. Can I ask you to be more concrete? What does "math is toast" mean to you?
- n4r9 11mo ago
  I'd like to see some other instances from your list.
- vatsachak 11mo ago
  In the sense that in 15 years my bet is that an AI system can solve my thesis problem for under 100$ https://ems.press/journals/jems/articles/14298293 https://ems.press/journals/jems/articles/14298293
  - emil-lp 11mo ago
    Math is toast if a computerized system can solve a problem you personally failed to solve during your PhD? Computers have proved stuff people couldn't since at least 1976 when Appel and Haken proved the 4-color theorem.
    - vatsachak 11mo ago
      The paper I linked is the problem I solved for my thesis, which was published in JEMS (upper echelon journal). I spent 8 hours a day for one and a half years working on it. 75% of mathematicians don't have a theorem that good, but the Terry Taos of the world get a theorem like that every year. My claim is that in 15 years an AI system will be able to prove it from first principles for under 100 dollars. That would render us normal mathematicians toast.

harshitaneja 11mo ago

The amount of goal post shifting is so amusing to see. Yes, sure this was probably not an "important" or a particularly "challenging" problem which had been open for a while. Sure, maybe it remained open because it didn't get enough eyeballs from the right people to care about spending time on it. Yes, there is too much overhyping and we are all tired of it somewhat. I still think if someone 10 years ago told me we would get "AI" to a stage where it can solve olympiad level problems and getting gold medals in IMO on top of doing so with input not in a very structured input but rather our complex, messy human natural language and being able to do so while interpreting, to various degrees of meaning what interpreting means, image and video data and doing so in almost real time I would have called you nuts and this thing in such a duration sci-fi. So some part of me feels crazy how quickly we have normalized to this new reality. A reality where we are talking about if the problem solved by the automated model using formal verification was too easy. Don't get me wrong, I am not saying any of this means we get AGI or something or even if we continue to see improvements. We can still appreciate things. It doesn't need to be a binary. What a time to be alive!

Davidzheng 11mo ago
Yeah, I agree. As a mathematician it's easy to say that it's not a super hard proof. But then again, the first proofs found by running AI on a large bucket of open problems was always going to be some easy proofs on a not-very-worked-on problem. The fact that no one did it before them definitely shows real progress being made. When you're an expert, it's hard to lose track of the fact that things that you consider trivial vs very hard may be in fact a very small distance in the grand scheme of things (rel to entities of different oom strengths)
magicalist 11mo ago
> The amount of goal post shifting is so amusing to see Can you be specific about the goal posts being shifted? Like the specific comments you're referring to here. Maybe I'm just falling for the bait, but non specific claims like this seem designed just to annoy while having nothing specific to converse about. I got to the end of your comment and counting all the claims you discounted, the only goal post I see left is that people aren't using a sufficiently excited tone while sifting fact from hype? A lot of us follow this work pretty closely and don't feel the need to start every post with "there is no need for excitement to abate, still exciting! but...". > I am not saying any of this means we get AGI or something or even if we continue to see improvements. We can still appreciate things. It doesn't need to be a binary. You'll note, however, that the hype guys happily include statements like "Vibe proving is here" in their posts with no nuance, all binary. Why not call them out?

kelseyfrog 11mo ago

An Erdos problem is great, but all major LLMs still score 0 out of 7 on all Millenium Prize Problems[1]. I, and I'm sure other like me, won't consider it "true" AI until AI saturate the MillenniumPrizeProblemBench. 1. https://www.claymath.org/millennium-problems/ https://www.claymath.org/millennium-problems/ 1.

jfengel 11mo ago
That's interesting, because what I'm looking for from AI is the opposite. Rather than looking to do something humans find hard, I'm more interested in the problems that humans find easy, like driving a car or counting the number of "r"s in a word. Having it go beyond that to do things that we can't do would be a nice bonus. But given the way AI has been going, I'd say there's a decent chance that it solves a Millennium Prize problem before it solves driving.