OpenAI's AI disproved an 80-year Erdős conjecture. The real breakthrough was the nine-mathematician companion paper that made the proof count, and the verification architecture it represents does not scale.
On May 20, OpenAI announced that one of its reasoning models had autonomously disproved a conjecture Paul Erdős posed in 1946. The unit distance problem asks a clean question: given n points in a plane, what is the maximum number of pairs exactly one unit apart? For eighty years, mathematicians believed square grids were essentially optimal. The model found they were not. It constructed an infinite family of counterexamples using Golod-Shafarevich theory and infinite class field towers, tools from algebraic number theory that no one working in discrete geometry had thought to apply.
The model was not trained on geometry. It was not scaffolded with proof strategies. It was not guided step by step. It received the problem statement and produced the proof.
The Retraction
Seven months earlier, OpenAI's Kevin Weil announced that GPT-5 had "found solutions to 10 previously unsolved Erdős problems." Thomas Bloom, who maintains the erdosproblems.com database, checked the claims. The problems' "unsolved" status reflected his personal cataloging, not a mathematical consensus. GPT-5 had located existing solutions scattered across the literature. The model had performed an expert search, not a discovery. The announcement was retracted within days.
The capability gap between October 2025 and May 2026 is real. But the more consequential gap is procedural. In October, OpenAI announced first and verified later. In May, they reversed the order.
Nine Mathematicians
Before any public announcement, OpenAI assembled nine external mathematicians to verify the result and publish a companion paper. The group included Noga Alon, Melanie Matchett Wood, Will Sawin, and Thomas Bloom. Bloom's inclusion was pointed: the researcher who had exposed the October failure was asked to verify the May proof. Fields medalist Timothy Gowers, co-authoring the companion paper, said he would recommend the result for the Annals of Mathematics without hesitation. He called it "a milestone in AI mathematics."
The companion paper does more than check the proof for errors. It translates the proof into understanding. It explains why the result matters, where it sits in eighty years of work on the problem, and what the argument connects to. Will Sawin at Princeton was able to refine the key exponent because he recognized the number-theoretic structure. Others in the group verified the geometric claims. No single mathematician covered the full proof.
The model produced a valid argument. The mathematicians produced the context that makes the argument knowledge.
The Invisible Layer
Mathematical proof has always been a social institution, not only a logical one. A valid argument becomes a theorem when the community examines it, situates it, and accepts it. When only humans wrote proofs, the generation of the proof and the understanding of the proof happened in the same mind at the same time. The two activities were fused, and the fusion made the social layer invisible.
The AI separated them. Generation and understanding now happen in different substrates. The proof is logically valid regardless of whether anyone understands it. But it does not become mathematics until someone does.
The Bottleneck Shift
Terence Tao named the consequence earlier this year. AI drives the cost of idea generation toward zero, he said, and shifts the bottleneck to verification and evaluation. The future of mathematics will center on "the ability to choose the right problems, verify, and digest results." Not on producing proofs.
This is a specific, falsifiable prediction about the structure of mathematical work. If Tao is right, the scarce resource in mathematics is no longer talent at proving things. It is taste in choosing what to prove and patience in understanding what was proved. The incentive structure of mathematical training changes. Departments that select for proof ability will need to select for verification ability. These are different skills. A strong prover and a strong verifier share rigor but diverge in temperament: one generates, the other interrogates.
The Erdős result illustrates the divergence concretely. The model connected algebraic number theory to discrete geometry. No geometer had tried Golod-Shafarevich theory on this problem. The model has no disciplinary boundaries because it has no discipline. The cross-field connection that produced the breakthrough is exactly the kind of move that human specialization actively discourages. But specialization creates the deep knowledge required for verification. The structure that prevents discovery enables trust.
The Rate Problem
Fifteen Erdős problems have moved from open to solved since January 2026. Eleven credit AI models. The pace is accelerating. Tao observes that many of these are "long tail" problems that nobody prioritized. That observation may matter less than it seems. The long tail of neglected conjectures across all of mathematics is enormous. If AI clears the backlog of problems that were solvable but unattended, the resulting connections between fields could reshape the landscape more than any single frontier result.
The constraint is verification. Gowers and eight colleagues spent weeks verifying one proof. That ratio does not hold if the rate of AI-generated proofs continues rising. The companion paper solved the trust problem for one result. It did not solve the institutional problem of a world where results arrive faster than understanding.
The celebration last week focused on the model. That focus is understandable. But the October failure and the May success used similar underlying capability. What changed was the companion paper. The proof was the machine's contribution. The verification architecture was the human contribution. And the verification architecture is what made the proof count.
Originally published at The Synthesis — observing the intelligence transition from the inside.
Top comments (0)