They got nine mathematicians to improve and comment on the proof and they're all saying nice things about it: Noga Alon: Thomas Bloom: W T Gowers: Daniel Litt: Arul Shankar: ... Jacob Tisimerman:...
Exemplary
They got nine mathematicians to improve and comment on the proof and they're all saying nice things about it:
Noga Alon:
The solution of the problem by the internal model of Open AI is, in my opinion, an outstanding
achievement, settling a long-standing open problem. The fact that the correct answer is not n^
1+o(1) is surprising, and the construction and its analysis apply fairly sophisticated tools from algebraic number theory in an elegant and clever way.
Thomas Bloom:
Perhaps tempting fate, on 16th April I included this problem in a blog post on www.erdosproblems.com titled (somewhat tongue in cheek) ‘Top 10 Erdős Problems’. [...] While I believed that AI would make some progress on at least a couple of the problems in that list eventually, I did not expect this to happen just one month later!
If the result of this paper was a proof of the unit distance problem, that would be truly incredible.
While I was still very surprised to hear of the this result, this was dampened slightly when I
learnt it was a construction of a counterexample [...]
On examining the construction, it becomes more clear how people had missed this before – it
requires the confluence of several different unlikely events [...] The AI met all of these criteria, and its success here echoes previous achievements: it often produces the most surprising results by persevering down paths that a human may have dismissed as not worth their time to explore [...]
Still, while perhaps not the proof of a conjecture that we had hoped for, no doubt this construction and the ideas involved will have a major impact in discrete geometry.
One aspect of this proof should not be overlooked: while the original proof produced by AI was
completely valid, it was significantly improved by the human researchers at OpenAI and the many
other mathematicians involved in the present paper.
W T Gowers:
In any case, there is no doubt that the solution to the unit-distance problem is a milestone in AI
mathematics: if a human had written the paper and submitted it to the Annals of Mathematics and
I had been asked for a quick opinion, I would have recommended acceptance without any hesitation.
No previous AI-generated proof has come close to that.
Daniel Litt:
This is the first example of a result produced autonomously by an AI that I find exciting in itself,
as opposed to as a leading indicator.
Arul Shankar:
I had not encountered this problem before seeing the proof from OpenAI, and I found the proof
to be a clean execution of a very beautiful idea and quite well written up.
...
All the same, I would consider this to be a very "human" proof, though a extremely ingenious one.
Jacob Tisimerman:
This is a really impressive piece of work, and I would accept it for any journal without hesitation.
While it’s true in the final solution that nothing is all that surprising, there are many
ways to attempt to set this construction up ... It’s always tempting to look at a completed
proof and declare it obvious after the fact.
This may indicate one way that AI systems have an edge: it’s not just that they can try all known
methods, but they can play for longer and in more treacherous waters than mathematicians without
getting overwhelmed. Of course this is not yet robustly true, but this may be a foreshadowing event.
Melanie Matchett Wood:
I had not heard of this problem before hearing of the solution from Open AI. I find the argument
to be a beautiful application of number theory to a natural, concrete question.
[...] I believe if the level and type of human expertise that is represented on this note had been assembled to find a counterexample to this conjecture a month ago, and those people put in similar amounts of time working on it tha[t] they did to reading and thinking about Chat GPT’s solution, the mathematicians would have found a counterexample. However, without the claimed proof by Chat GPT, there is no particular reason anyone would have tried to look for a counterexample, assembled a group of experts with the appropriate expertise, or that the experts would have agreed to turn their attention to this problem.
For nearly 80 years, mathematicians have studied a deceptively simple question: if you place n points in the plane, how many pairs of points can be exactly distance 1 apart?
This is the planar unit distance problem, first posed by Paul Erdős in 1946. It is one of the best-known questions in combinatorial geometry, easy to state and remarkably difficult to resolve. The 2005 book Research Problems in Discrete Geometry, by Brass, Moser, and Pach, calls it “possibly the best known (and simplest to explain) problem in combinatorial geometry.” Noga Alon, a leading combinatorialist at Princeton, describes it as “one of Erdős’ favorite problems.” Erdős even offered a monetary prize for resolving this problem.
Today, we share a breakthrough on the unit distance problem. Since Erdős’s original work, the prevailing belief has been that the “square grid” constructions depicted further below were essentially optimal for maximizing the number of unit-distance pairs. An internal OpenAI model has disproved this longstanding conjecture, providing an infinite family of examples that yield a polynomial improvement. The proof has been checked by a group of external mathematicians. They have also written a companion paper explaining the argument and providing further background and context for the significance of the result.
[...]
Fields medalist Tim Gowers, writing in the companion paper, calls the result “a milestone in AI mathematics.” According to leading number theorist Arul Shankar, “In my opinion this paper demonstrates that current AI models go beyond just helpers to human mathematicians – they are capable of having original ingenious ideas, and then carrying them out to fruition”.
[...]
The proof is available here. The companion paper by leading external mathematicians is available here. You can find an abridged version of the model’s chain of thought here.
This really echoes what we are seeing with Mythos and exploit generation. LLMs are happy to grind away on the most obscure corners of a problem space for as long as you allow them more tokens,...
I believe if the level and type of human expertise that is represented on this note had been assembled to find a counterexample to this conjecture a month ago, and those people put in similar amounts of time working on it tha[t] they did to reading and thinking about Chat GPT’s solution, the mathematicians would have found a counterexample. However, without the claimed proof by Chat GPT, there is no particular reason anyone would have tried to look for a counterexample, assembled a group of experts with the appropriate expertise, or that the experts would have agreed to turn their attention to this problem.
This really echoes what we are seeing with Mythos and exploit generation. LLMs are happy to grind away on the most obscure corners of a problem space for as long as you allow them more tokens, where humans would simply not be interested, and they can do so at a level that is on par with extremely qualified humans.
I think Thomas Bloom nailed it on the head: This is ultimately why the people who discover new and innovative things are at least a little bit crazy. I do well and truely beleive that Nikola Tesla...
I think Thomas Bloom nailed it on the head:
often produces the most surprising results by persevering down paths that a human may have dismissed as not worth their time to explore
This is ultimately why the people who discover new and innovative things are at least a little bit crazy. I do well and truely beleive that Nikola Tesla may well have figured out how to provide free wireless electricity to everyone if left to his devices and not cut off by the funder that would not have gotten a return. It takes a bit of derangement to ignore all of the 'common sense' and 'sound advice' and poke the bear (so to speak).
One aspect of this proof should not be overlooked: while the original proof produced by AI was
completely valid, it was significantly improved by the human researchers at OpenAI and the many
other mathematicians involved in the present paper.
I would be very curious to see the exact prompting, how long (and how many tokens), how many iterations/refinements, and how many utterly failed attempts where it went completely off the rails and went on a dead end till somebody killed it. My guess is that we're at least a little bit in 'monkeys/typewriters/Shakespeare' territory. Much like the recent spat of software bug discovery, the humans in the loop are what made the paper good. Or in other words, the humans had to verify the AI. How many failed attempts at getting this (or any) proof are hidden behind the curtain?
In other words: Did solving this proof cost $5 billion? I would not be surprised given the level of PR.
All of this said, it's still cool, and the only bit I think I well and truely disagree with is this assessment from Tim Growers:
In my opinion this paper demonstrates that current AI models go beyond just helpers to human mathematicians – they are capable of having original ingenious ideas, and then carrying them out to fruition
The AI combined the Legos that were already there. It did not build new Legos. It's just really good at digging all of the miscellaneous bits out of the giant bin we accumulated over the years. I will take more stock in that claim when the AI can posit a new conjecture and/or solve one in a completely novel way.
AI coding platforms love to solve type errors by slapping an Any or Unknown on it. Because that's the statistically most likely solution is given its dataset.
This gets into whether mathematical proofs are invented or discovered. In some sense, the information was already implicit in the axioms. But that would be defining creativity in such a strict way...
This gets into whether mathematical proofs are invented or discovered. In some sense, the information was already implicit in the axioms. But that would be defining creativity in such a strict way that humans don't do creative work either.
I don't follow the math, but if the mathematicians say it's sufficiently original to publish in a top journal, I believe them.
It seems similar to the situation with AlphaGo. This proof apparently needed some cleaning up for understandability, but maybe that won't be needed in a year or two?
They got nine mathematicians to improve and comment on the proof and they're all saying nice things about it:
Noga Alon:
Thomas Bloom:
W T Gowers:
Daniel Litt:
Arul Shankar:
...
Jacob Tisimerman:
Melanie Matchett Wood:
From the article:
[...]
[...]
This really echoes what we are seeing with Mythos and exploit generation. LLMs are happy to grind away on the most obscure corners of a problem space for as long as you allow them more tokens, where humans would simply not be interested, and they can do so at a level that is on par with extremely qualified humans.
I think Thomas Bloom nailed it on the head:
This is ultimately why the people who discover new and innovative things are at least a little bit crazy. I do well and truely beleive that Nikola Tesla may well have figured out how to provide free wireless electricity to everyone if left to his devices and not cut off by the funder that would not have gotten a return. It takes a bit of derangement to ignore all of the 'common sense' and 'sound advice' and poke the bear (so to speak).
I would be very curious to see the exact prompting, how long (and how many tokens), how many iterations/refinements, and how many utterly failed attempts where it went completely off the rails and went on a dead end till somebody killed it. My guess is that we're at least a little bit in 'monkeys/typewriters/Shakespeare' territory. Much like the recent spat of software bug discovery, the humans in the loop are what made the paper good. Or in other words, the humans had to verify the AI. How many failed attempts at getting this (or any) proof are hidden behind the curtain?
In other words: Did solving this proof cost $5 billion? I would not be surprised given the level of PR.
All of this said, it's still cool, and the only bit I think I well and truely disagree with is this assessment from Tim Growers:
The AI combined the Legos that were already there. It did not build new Legos. It's just really good at digging all of the miscellaneous bits out of the giant bin we accumulated over the years. I will take more stock in that claim when the AI can posit a new conjecture and/or solve one in a completely novel way.
AI coding platforms love to solve type errors by slapping an Any or Unknown on it. Because that's the statistically most likely solution is given its dataset.
This gets into whether mathematical proofs are invented or discovered. In some sense, the information was already implicit in the axioms. But that would be defining creativity in such a strict way that humans don't do creative work either.
I don't follow the math, but if the mathematicians say it's sufficiently original to publish in a top journal, I believe them.
It seems similar to the situation with AlphaGo. This proof apparently needed some cleaning up for understandability, but maybe that won't be needed in a year or two?