Among the hundreds of results OpenAI released to the mathematics community this week are proofs relevant to 23 problems from the Erdős problems database, according to Thomas Bloom, who runs Erdosproblems.com. In a blog post on Thursday, Bloom said that all 23 are, in his view, interesting and significant.
OpenAI released its GitHub repository on Tuesday, October 6, containing 372 significant proof claims across pure mathematics. Bloom has gone through the release and compiled the ones that touch his site.
The problems
The 23 Erdős problems with claimed results are numbers 3, 90, 120, 138, 148, 172, 181, 184, 293, 304, 371, 416, 431, 508, 551, 604, 802, 821, 952, 968, 970, 1083 and 1150. Twelve of them (3, 138, 172, 181, 184, 371, 431, 508, 821, 952, 970 and 1083, with 508 only partially) are on the FrontierMath Erdős list.
Some of the headline claims:
- Problem 3 (arithmetic progressions): A quasipolynomial-type bound for Szemerédi’s theorem for all progression lengths, which would imply Erdős’s famous conjecture that a set of integers whose reciprocals sum to infinity contains arbitrarily long arithmetic progressions. The paper runs to 198 pages. Bloom notes that the accompanying Lean file currently only proves a weaker bound.
- Problem 90 (unit distances): A new upper bound showing that n points in the plane determine at most n^(4/3−c) unit-distance pairs, improving on the long-standing n^(4/3) bound of Spencer, Szemerédi and Trotter. The PDF doesn’t give a value for c.
- Problem 508 (chromatic number of the plane): A claimed proof that any 5-colouring of the plane has two same-coloured points at distance one, which would mean the chromatic number of the plane is 6 or 7.
- Problem 181 (hypercube Ramsey numbers): The Ramsey number of the n-dimensional hypercube is O(2^n), a conjecture of Burr and Erdős. The paper is 172 pages long and has not been formalised.
- Problem 184 (cycle decompositions): Any n-vertex graph can be split into O(n) edge-disjoint cycles and edges, improving on a previous bound with an extra iterated-logarithm factor.
- Problem 138 (van der Waerden numbers): A lower bound confirming Erdős’s conjecture that the two-colour van der Waerden number grows faster than any exponential in k.
- Problem 431 (primes and sumsets): A proof of Ostmann’s conjecture, sometimes called the inverse Goldbach problem.
- Problems 148, 293 and 304 (unit fractions): Best-possible bounds on writing fractions and 1 as sums of distinct unit fractions, in one 33-page paper.
- Problem 172 (Hindman’s conjecture): For any finite colouring of the positive integers, there are arbitrarily large sets whose sums and products all share one colour.
- Problem 1083 (distinct distances): At least n^(2/d) distinct distances for n points in d-dimensional space, which Bloom notes is stronger than Erdős’s own conjecture.
The list also includes results on totient values (416 and 821), prime gaps (968), the Gaussian moat problem (952), Jacobsthal’s function (970), the largest prime factors of consecutive integers (371), independent sets in clique-free graphs (802), Ramsey numbers of cycles and complete graphs (551), pinned distances (604), ultraflat Littlewood polynomials (1150), and a special case of the Erdős similarity problem (120).
Nineteen of the 23 results come with Lean formalisations. The four that don’t are 172, 181, 821 and 1083. Together, the papers add up to 1,268 pages, or about 55 pages per problem.
Caveats from Bloom
Bloom is careful to say that he hasn’t yet looked seriously at any of the proofs, and hasn’t checked that the Lean formalisations compile or that the formal statements capture the original problems accurately. He says his post is a summary of claims and not an endorsement.
The papers, he says, are poorly written in the usual AI fashion, though he expects most to be correct and capable of being simplified substantially with expert attention. He suggests treating them as “very rich raw material” and not finished mathematics.
He also stresses that none of the problems should be considered closed to human researchers. There is still a great deal of work to do in reading, verifying, simplifying and explaining the proofs, and human approaches that differ completely from the AI’s may well exist.
That tension is already playing out. Terence Tao has criticised the way so many proofs were released at once, arguing that it makes math less fertile, while a new mathematicians’ group has accused OpenAI of disregarding the norms of scientific research. OpenAI, for its part, says it consulted the Institute for Advanced Study’s advisory group on mathematics and AI in deciding how to share the results.
AI and Erdős problems
The Erdős problems database has become one of the most closely watched benchmarks for AI in mathematics, and this release is the latest, and by far the largest, step in a progression that has been moving quickly.
The story hasn’t been smooth. In October 2025, claims that GPT-5 had solved ten Erdős problems fell apart after it emerged that the model had mostly surfaced existing solutions from the literature. Bloom himself was among the critics.
That changed in January 2026, when GPT-5.2 Pro produced what Tao described as a more-or-less autonomous solution to Problem 728, followed by others including Problems 729 and 397, with Harmonic’s Aristotle formalising proofs in Lean. Problem 281 followed soon after, although it was later found that a prior solution already existed in the literature, so it was reclassified. Tao nonetheless noted that the AI’s proof was rather different from the earlier ones. Tao has also cautioned that these early wins tended to be the lowest-hanging fruit, and that only a small percentage of open Erdős problems were simple enough for AI to handle with minimal human help.
The bigger moment came on May 20, when OpenAI announced that an internal general-purpose reasoning model had disproved Erdős’s 1946 conjecture on the planar unit distance problem (Problem 90), producing configurations of points with polynomially more unit-distance pairs than the square-grid constructions that were long believed to be optimal. A group of external mathematicians, including Bloom, checked the proof and co-wrote a companion paper, and Princeton’s Will Sawin later made the exponent explicit. The new release returns to the same problem from the other side: the May result was a lower bound, while the new claim is an improvement on the upper bound.
If the new proofs hold up, the shift from picking off easy problems to tackling some of the best-known open questions in combinatorics, number theory and geometry will be significant. For now, though, the verification work is only beginning, and 1,268 pages is a lot to read.