On AI mathematics

One of our key uncertainties is whether LLMs will scale all the way to "AGI" in any strong sense. A further uncertainty, inside that, is whether they can do AI research in any strong sense, and that in turn depends on them having "research taste" (originality, creativity, good judgment about latent variables).

A domain which is easier for us to check is research mathematics, and so we've spent a good amount of time this year tracking the explosion of AI-assisted and autonomous solves of open research questions.

The Erdős era#

How should we think about the era where "vertical generalization" (the ability of the best systems to keep improving within a domain they are trained for) is demonstrated - but, in mathematics, more or less exclusively for Erdos problems? Some notes:

• Erdos problems are not definitionally important, famous, or profound -- it’s just a list of every conjecture Erdos ever made in writing. There are currently about 600 open Erdos problems. A minority within that list of 600 problems are considered very difficult (in the sense of ‘very strong specialists spent a lot of time on them’) but arguably ‘shallow’ problem, such as Erdos #90 aka The Unit Distance Problem solved by OpenAI. A much smaller minority are believed to be both very, very difficult and very deep.

• The original, legitimate role of saying ‘AI solved an open Erdos problem’ was strictly to certify non-triviality. If a proposition/question is an ‘Erdos problem’ it means a strong mathematician (Erdos) thought it’s worthwhile to write it down -- and so that it’s at least a little mathematically interesting. If the proposition/question is furthermore an open Erdos problem, you also get defeasible evidence that even in the ‘00s the problem is not so easy that any pro mathematician can do it on the spot. (Since, at the least, the mathematicians running the Erdos problems website gave each problem a quick look.)

• There was also always a PR side-effect to the ‘Erdos problems’ meme. Many technical people outside pure math assume that, because Erdos is so famous, an ‘Erdos problem’ (e.g. one of the 1200+ conjectures Erdos made) should be comparable to a ‘Hilbert problem’ (e.g. one of the 24 deepest questions statable by early C20th math) or a ‘Millenium problem’.

• Is anything happening outside of Erdos-land? GDM’s new paper states -- and demonstrates -- that their new agent proved a result in algebraic geometry, often considered a more truly ‘higher math’ area. HOWEVER Daniel Litt told us in private that the result ('Log-Concavity of Hilbert Sequences') was algebraic geometry in name only. Per Litt it is unmistakably ‘combinatorial’/’Erdosy’ math, and not of interest to the kind of algebraic geometers that gave the subfield its reputation for profundity.

• GDM are again using a complex hybrid LLM/Lean-verifier system with a carefully tuned domain-specific harness. OpenAI claim that their internal model that cracked Erdos #90 was ‘a general reasoning model’ not specialized for mathematics. Unclear what this means -- does it mean no special harness? No in-harness finetuning? No Lean?

• But it gets (epistemically) even worse: Our own experiments -- alongside similar work by others -- gave us early indication that GPT 5.5 Pro can recreate the proof of Erdos #90. So it’s unclear if OpenAI’s “internal general reasoning model” Erdos #90 solve demonstrates any new rise in the power of ‘general reasoning’ models. We’d need to know exactly what OpenAI’s discovery process for targeting Erdos #90 was to know if their process relied on a jump in model capabilities.

Overall we (i.e. the culture) are in epistemic hell when it comes to the cutting-edge research-math capabilities of frontier models. We’re short on appropriately contextualized info about results are being churned, and we face a theoretical/philosophical challenge when it comes to evaluating the significance of hard-Erdos-math ability as a leading indicator of “true” intellectual ability:

• P3’s current modest empirical intervention is to spend some compute systematically testing what models from subsequent recent generations can and can’t prove and how often.

• On the theoretical/philosophical side, more mathematicians are now asking themselves whether a certain archetype of mathematical snob -- e.g. an algebraic topologist or K-theorist or noncommutative geometrist who always regarded Erdos-style math as unserious, and who regards even Fields medalists like Timothy Gowers or Terry Tao as doing a ‘light’ type of mathematics -- was on to something.

• Daniel Litt’s Problems I Like is, in our opinion, the next frontier. Problems that are pre-registered as serious and substantive in Litt’s problem collection (the collection also contains problems pre-registered as curiosities) are expressive of Litt’s taste for problems that have crunch to them but would not elicit dismissal as depthless from depth-first mathematicians.

See also a recent interesting essay on LLM mathematics from a poasting French mathematician:

...If the proliferation of bogus proofs produced by incompetent AI forces us to convert all mathematics into formal language (including proofs supposedly produced by humans because we can no longer be certain), it will represent a massive setback for our [mathematics’] capabilities.

... [OAI’s Erdos 90 proof was] relatively untechnical, easy to prove, and require no complicated tools, but which still needed to be "thought" to be introduced. (The difficult part of the proof… is a standard technique known to experts. …their silence on the time or computing power is very telling…)

... There is a very credible possibility that AI will simply put an end to the human adventure in mathematics… by destroying the economic foundations of the practice of mathematical research; or at the very least, that it will lead to reserving the practice of mathematics for the wealthiest, who will be able to afford access to top-of-the-line, deluxe AI .

...The LLM seems to have beaten humans on this problem for three main reasons: it wasn't influenced by Erdős's intuition, it has an encyclopedic knowledge of mathematics, and it has inexhaustible patience for exhaustively testing avenues combined with a total intention to solve this problem and this problem specifically. On the other hand, there's no trace of a flash of intuition, a new technique, much less superhuman genius ( at this stage ). This is roughly how I interpret the current situation. We must neither overestimate this result ( current LLMs are absolutely not superhuman[ #20 ] in math), nor underestimate it (they are not stochastic parrots either, as some like to say).

Erdos #90#

This is the first really major AI mathematical result: an internal OAI “general” model disproving a classic 1946 Erdos conjecture in discrete geometry.

It's a counterexample, and counterexamples are the cheapest kind of proofs, but this one used deep machinery and gave a constructive recipe: so a major world-class result. Could have been two or three steps deeper if it gave a structural theorem or a dictionary or had effective parameters, but this is saying that your 20-second 100m sprint could have been a 9 second one.

1500 pages of reasoning → 125 page summary released → 16 page AI proof → 3 page human proof

Before AI, there were likely 20-100 years of failed human efforts to solve it. The summarised CoT is 125 pages; could guess that it was 5-32 hours clock time, $120 - $10000 of tokens. Supposedly not math specialised, not using Lean as intermediate representation, nor even math-specific scaffolded. At least three models involved: problem drafter, evaluator, and solver. some signs that they might be spawning conjectures en masse as part of a complicated training scheme.

Alon et al "somewhat simplified and somewhat generalized” the AI result, and within days Sawin seriously improved on the AI proof. But the initial loose solve was autonomous.

The OAI proof was a disproof by counterexample, but it was a nice parametrised one. In some sense it’s very deep (y-axis):

The OAI proof “reduces” to Golod–Shafarevich towers + Ellenberg–Venkatesh's ell-torsion in reverse + Hajir–Maire–Ramakrishna but that ignores all the details it also got right and even applying these together is highly nontrivial. It is easy to say that it is not superhuman and was knowledge bottlenecked.

In the model’s own words: “Suppose optimistically that K is a high-degree CM field… Then the construction is frightening.”

Our reproduction attempts#

Inspired by Gowers’ commentary of the result, we’ve been running experiments with previous- and current-gen models (GPT-5.4-Pro, GPT-5.5-Pro, Gemini models, Chinese models) to better understand just how difficult reproducing this result is when the prompt includes various hints about the right approach.

The reference prompt we have been using is the following

Define ν(P) \= |{ {p,q} ∈ (P choose 2\) : ||p−q||₂ \= 1 }| and, for each integer n ≥ 1, ν(n) \= max\_{P⊂R², |P|=n} ν(P).

Resolve Erdős's planar unit-distance problem completely: ν(n) ≤ n^{1+O(1/log log n)} as n → ∞? Equivalently, determine whether there exist absolute constants C \> 0 and N ∈ ℕ such that ν(n) ≤ n^{1+C/log log n} for every integer n ≥ N. Here log denotes the natural logarithm, and N may be taken large enough that log log n \> 0\. The hidden constant in O(1/log log n) is absolute and independent of P and n.

A complete solution must prove exactly one of the following.

Affirmative resolution. Prove that there exist absolute constants C \> 0 and N ∈ ℕ such that every set P ⊂ R² of n ≥ N distinct points satisfies ν(P) ≤ n^{1+C/log log n}.

Negative resolution. Prove that no such constants exist. Equivalently, prove that for every C \> 0 and every N ∈ ℕ, there are an integer n ≥ N and a set P ⊂ R² of n distinct points such that ν(P) \> n^{1+C/log log n}.

Pairs are unordered, the distance is the usual Euclidean distance in R², and the asymptotic assertion is for all sufficiently large integers n, not merely infinitely many n.

Partial progress does not count unless it implies one of the two resolutions above. In particular, improved bounds such as O(n^{4/3−ε}), better constants in the n^{4/3} bound, finite verification, special cases, structural reductions, or heuristic evidence are insufficient unless they prove the full Erdős bound or disprove it.

Do not use web search. Solve this entirely from your own reasoning and internal knowledge.

Hints, in order.  
{HINTS}

This problem has just been solved. You are being asked to solve it here as a test of your capabilities. It is thus critical that you try your best and not search the web.

The hints we’ve been using as part of our experiments are

• (i) Look for a counterexample.
• (i) Look for a counterexample.
  (ii) Take the best known construction and generalize it.
• (i) Look for a counterexample.
  (ii) Take the best known construction and generalize it.
  (iii) Replace what you were previously trying to prove by a non-uniform version, but work with prime ideals of bounded norm.

Our findings are preliminary. Still, what we have found so far is that:

• GPT-5.5-Pro
  • With a single hint (see runs 1, 2, 3, 4, 5) claimed a successful disproof in 1 out of 5 attempts.
  • With two hints (see runs 1, 2, 3, 4, 5) claimed a successful disproof in 2 (see here and here) out of 5 attempts.
• GPT-5.4-Pro
  • With a single hint (see runs 1, 2, 3, 4, 5) claimed a successful disproof in 2 out of 5 attempts, though only one seems to pass 5.5-pro’s evaluation.

More experiments are ongoing, including with 5.4 and 5.5 Thinking variants, and with chinese models as well. So far though, my conclusion is that the solution found by 5.6-Pro or whatever internal model OpenAI used for this result has been reachable by current and previous -Pro models (at least up to the 5.4 generation), but that when given only the problem in the prompt, the models likely spend too much time trying to prove the conjecture affirmatively (rather than seeking to disprove it via a counterexample). This reminds me of what Gowers and others say in the commentary: Gowers says it had not occurred to him to try to disprove it, Tsimerman says he had briefly tried counterexamples and failed, and Wood’s comment is basically: assemble the right number theorists and geometers and they might have found it, but nobody had a reason to assemble them for a counterexample search.

See also#

Poor Deepmind. They solve 9 Erdos problems at the same time OAI solves a famous one, and get totally ignored.

See also a Litt-checked proof that Mythos also manages to prove Erdos #90 in a similar fashion to OAI.

Sebastian Bubek of OAI also believes that recent attempts to prove Erdos #90 using GPT 5.5 with trivial human interaction produce valid proofs.