Thomas Bloom lists 25 Erdős problems in OpenAI’s release: not yet checked, though he expects most to hold up

What happened

• On October 6, 2026, OpenAI published 722 math manuscripts, grouped into 372 families, written by an unreleased AI model (see the entry on the 722 manuscripts). Thomas Bloom describes the release as "372 significant proof claims in mathematics."
• On October 8, Bloom, who runs erdosproblems.com, a public database of open problems posed by the Hungarian mathematician Paul Erdős, posted a list of the problems in that release that are relevant to the site.
• He counts significant claims on 25 Erdős problems. His list does not sort all 25 into full solutions and partial results, though at least one claim, on problem 508, is a partial solution. Twelve of the 25, problem 508 among them, are on the FrontierMath Erdős list, a set of Erdős problems used to test AI systems.
• For 21 of the 25, the release includes a version of the proof in Lean, a programming language for proofs. If a Lean file compiles with no `sorry` placeholders and no extra axioms, a computer has checked every step of the proof, but only of the statement and definitions as written in Lean. Bloom says he has not yet checked that those files compile, or that each Lean statement says the same thing as the original problem. So "formalized in Lean" here means OpenAI supplied the files; as of this post, Bloom had not confirmed that they check.
• The written proofs, as PDFs, total 1,347 pages, about 54 pages per problem. Bloom notes that a proper discussion of each claim needs someone to read both the PDF and the earlier literature on the problem.
• One claim is on problem 90, the unit distance problem: among n points in the plane, how many pairs can be exactly one unit apart? The best known upper bound was n to the power 4/3. The release claims n to the power 4/3 minus c, for some fixed c greater than 0, which would lower the exponent itself. Bloom notes that the PDF gives no indication of the value of c.
• Another is a proof of a conjecture of Burr and Erdős about the n-dimensional cube, which has 2 to the n corners (problem 181, one of the four without a Lean version). Take some number of points, connect every pair with a line, and color each line red or blue: how many points do you need before one color must contain a copy of the cube? Burr and Erdős conjectured that a constant times 2 to the n points always suffice, and that is what the release claims to prove.
• Bloom says the post makes no judgment about novelty or credit, and that the PDFs may leave out important references.

What people said