Remix.run Logo
smokel 4 hours ago

How was that not the case? As far as I understand it ChatGPT was instrumental to solving a problem. Even if it did not entirely solve it by itself, the combination with other tools such as Lean is still very impressive, no?

emil-lp 4 hours ago | parent [-]

It didn't solve it, it simply found that it had been solved in a publication and that the list of open problems wasn't updated.

Davidzheng 4 hours ago | parent | next [-]

My understanding is there's been around 10 erdos problems solved by GPT by now. Most of them have been found to be either in literature or a very similar problem was solved in literature. But one or two solutions are quite novel.

https://github.com/teorth/erdosproblems/wiki/AI-contribution... may be useful

carefree-bob an hour ago | parent | next [-]

I am not aware of any unsolved Erdos problem that was solved via an LLM. I am aware of LLMs contributing to variations on known proofs of previously solved Erdos problems. But the issue with having an LLM combine existing solutions or modify existing published solutions is that the previous solutions are in the training data of the LLM, and in general there are many options to make variations on known proofs. Most proofs go through many iterations and simplifications over time, most of which are not sufficiently novel to even warrant publication. The proof you read in a textbook is likely a highly revised and simplified proof of what was first published.

If I'm wrong, please let me know which previously unsolved problem was solved, I would be genuinely curious to see an example of that.

Davidzheng an hour ago | parent [-]

It's in the link above, but you can look at #1051 or #851 on the erdosproblems website.

carefree-bob 38 minutes ago | parent [-]

The erdosproblems website shows 851 was proved in 1934. https://www.erdosproblems.com/851

I guess 1051 qualifies - from the paper: "Semi-autonomous mathematical discovery with gemini" https://arxiv.org/pdf/2601.22401

"We tentatively believe Aletheia’s solution to Erdős-1051 represents an early example of an AI system autonomously resolving a slightly non-trivial open Erdős problem of somewhat broader (mild) mathematical interest, for which there exists past literature on closely-related problems [KN16], but none fully resolves Erdős-1051. Moreover, it does not appear to us that Aletheia’s solution is directly inspired by any previous human argument (unlike in many previously discussed cases), but it does appear to involve a classical idea of moving to the series tail and applying Mahler’s criterion. The solution to Erdős-1051 was generalized further, in a collaborative effort by Aletheia together with human mathematicians and Gemini Deep Think, to produce the research paper [BKK+26]."

Davidzheng 13 minutes ago | parent [-]

"The erdosproblems website shows 851 was proved in 1934." I disagree with this characterization of the Erdos problem. The statement proven in 1934 was weaker. As evidence for this, you can see that Erdos posed this problem after 1934.

emp17344 3 hours ago | parent | prev | next [-]

Some of these were initially hyped as novel solutions, and then were quietly downgraded after it was discovered the solutions weren’t actually novel.

Insanity 2 hours ago | parent [-]

Yeah that was also my take-away when I was following the developments on it. But then again I don't follow it very closely so _maybe_ some novel solutions are discovered. But given how LLMs work, I'm skeptical about that.

compass_copium an hour ago | parent | prev [-]

...am I wrong in thinking that 1(a) is the relevant section here, and shows a lot of red?

Davidzheng an hour ago | parent [-]

I honestly don't see the point of the red data points. By now all the erdos problems have been attempted by AIs--so every unsolved one can be a red data point.

3 hours ago | parent | prev [-]
[deleted]