For roughly 80 years, mathematicians believed Paul Erdős had the right intuition about how tightly you can pack points at equal distances in a plane. In May 2026, an AI reasoning model showed he was wrong — but understanding why requires knowing exactly what he claimed.
What Erdős's Unit-Distance Conjecture Actually Said
The unit-distance problem asks a deceptively simple question: given n points in the Euclidean plane, how many pairs can sit at exactly distance 1 from each other? Call that maximum ν(n) — the largest possible count of unordered point pairs separated by a unit distance across any n-point configuration . Erdős introduced the problem in 1946, and it became a central question in discrete geometry .
Erdős's lower-bound construction was grid-like: arrange points in a √n × √n integer-style grid, and you get ν(n) of order n1+o(1) . From that construction he conjectured a matching near-linear upper bound — that no configuration could do meaningfully better:
- The conjecture: ν(n) ≤ n1+O(1/log log n), where the exponent drifts toward 1 as n grows — meaning grids are essentially optimal .
- The formal statement: the Erdős Problems database lists this as Problem #90 — does every n-point planar set have at most n1+O(1/log log n) unit-distance pairs?
Two bounds framed the gap. The best known general upper bound is O(n4/3), with exponent ≈ 1.333, proved by Spencer, Szemerédi, and Trotter in 1984 — and unimproved for 40 years . (An elementary O(n3/2) bound follows from the unit-distance graph being K2,3-free.) Meanwhile the lower-bound exponent sat stuck at 1+o(1) for 80 years .
The sharp open question was whether any fixed δ > 0 exists such that ν(n) ≥ n1+δ for infinitely many n. A fixed positive δ would eventually exceed C/log log n for every constant C — formally breaking Erdős's near-linear ceiling and proving grids are not optimal . For decades, the prevailing intuition said no such δ existed. That intuition is what fell.
What Was Disproved — and What Endures
The theorem is precise and narrow: there exists some absolute constant δ > 0 such that ν(n) ≥ n1+δ for infinitely many n . The decisive word is fixed. Erdős's conjectured ceiling was n1+O(1/log log n) — an exponent whose excess over 1 shrinks toward zero as n grows. A fixed positive δ eventually exceeds C/log log n for every constant C, so the new construction punches through that ceiling for all large enough n and refutes the near-linear conjecture outright . Grids are not optimal.
What this is not matters as much as what it is. Headlines saying the AI "solved the unit-distance problem" overstate the claim. The model disproved a conjectured upper bound by exhibiting better point sets; it did not determine ν(n), and the exact asymptotic growth rate remains open . This is a lower-bound advance — a new floor under ν(n) — not a full resolution.
The other side of the gap is untouched. The best general upper bound, O(n4/3), proved by Spencer, Szemerédi, and Trotter in 1984, still stands . So after the breakthrough, ν(n) is pinned between an exponent of roughly 1.014 (the new explicit lower bound, from Sawin) and 1.333 (the SST upper bound) . That residual gap is wide and unresolved — the result narrows the space of plausible answers without closing it.
| Result | Bound on ν(n) | Type | Year |
|---|---|---|---|
| Erdős grid construction | n1+o(1) | Lower bound | 1946 |
| OpenAI model (existential) | n1+δ, δ > 0 unquantified | Lower bound | 2026 |
| Sawin (explicit) | n1.014114 | Lower bound | 2026 |
| Spencer–Szemerédi–Trotter | O(n4/3) ≈ n1.333 | Upper bound | 1984 |
The mathematical community framed the significance carefully, around the conjecture rather than the full problem. Noga Alon called it an outstanding achievement that settles a long-standing unsolved problem — language that fits a disproved conjecture, not a determined ν(n). For builders following the story, the precise scope is the point: a fixed-exponent improvement is qualitatively different from shaving a vanishing term, and it is exactly that qualitative jump, not a tidy closed-form answer, that fell here.
The Algebraic Number-Theory Bridge
The construction that broke the conjecture replaces the flat grid with machinery imported from algebraic number theory, and that import is the technically surprising part. Instead of arranging points on a √n × √n lattice, the model builds infinite towers of totally real number fields with bounded root discriminants — a property guaranteed by Golod–Shafarevich-type class-field-tower theory and the Hajir–Maire–Ramakrishna line of work . The bounded discriminants are what keep the eventual point set dense enough to beat the grid asymptotically.
From there the steps chain together as follows:
- Adjoin i to form CM fields. Each totally real field L is extended to K = L(i), a CM field, which supplies a complex structure to project into later .
- Use completely split rational primes. Primes that split completely in K produce many norm-one elements — algebraic units whose absolute value is exactly 1, the source of the unit distances .
- Embed into Minkowski lattices. Those elements sit inside high-dimensional Minkowski lattices built from the field's embeddings.
- Cut by a product-of-discs window. A product-of-discs filter selects a finite, well-controlled subfamily of lattice points.
- Project to one complex coordinate. Projecting onto a single complex coordinate collapses the high-dimensional set to a planar point set — one carrying many pairs at exactly distance 1 .
What mathematicians flagged as striking is the bridge itself: connecting class field towers and splitting primes to a discrete-geometry counting problem had no prior precedent. The companion arXiv note from Noga Alon and colleagues (arXiv:2605.20695, submitted 20 May 2026) reconstructs a short, human-verified version and, in retrospect, attributes the ingredients to Ellenberg–Venkatesh, Golod–Shafarevich, and Hajir–Maire–Ramakrishna ideas . Those are well-known tools individually; the contribution was wiring them into incidence geometry, where they had never been pointed before.
That cross-domain reach is also why the path eluded human researchers for so long. Exploiting class-field towers for a unit-distance construction demands breadth across number theory and combinatorial geometry that was not an obvious or rewarded direction. Notably, Jacob Tsimerman reportedly explored a similar line and abandoned it as too time-consuming — a "grind" of failed attempts rather than a missing insight .
"An outstanding achievement that settles a long-standing unsolved problem," — Noga Alon, mathematician and co-author of the companion note (source: Understanding AI).
For builders, the technique matters more than the headline. The win came not from inventing wholly new mathematics but from recombining established machinery across subfields that humans rarely traverse together — a profile of capability worth tracking as these models move into research workflows.
AI Autonomy and the Mathematician's Actual Contribution
The most contested claim in OpenAI's manuscript is procedural, not mathematical: the problem was, in its words, "solved in a completely automated fashion" . An AI-written problem statement went to an internal reasoning model, the model produced a solution, and an AI grading pipeline reported high confidence — all before any person read the argument . That is the autonomy worth taking seriously: not a chatbot answering a prompt, but a closed loop that posed, attempted, and pre-scored its own work.
What followed matters just as much. Only after the grading signal did OpenAI researchers and external mathematicians — Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood — examine, verify, rewrite, simplify, and strengthen the proof . Their companion note, arXiv:2605.20695, submitted 20 May 2026, is the human-digested version of the machine's counterexample — the artifact most mathematicians actually read and trust . The framing across every primary account is collaboration, not obsolescence: the AI generated a candidate; humans certified and improved it.
"The first AI-produced result I've found exciting in itself," — Daniel Litt, mathematician and co-author of the companion note (source: Understanding AI).
Two gaps should temper any product-level reading. First, the model is unnamed. The primary manuscript does not identify which internal system produced the result, and no public release — GPT-5, o3, or ChatGPT — is tied to it in any primary source . Headlines naming a shipped product are extrapolating beyond what OpenAI disclosed. Second, the process is not reproducible. OpenAI published no sampling protocol, compute cost, grading-pipeline internals, or training details . The output — a counterexample to Erdős's near-linear conjecture — is independently checkable by reading the math; the discovery pipeline that generated it is not.
For builders evaluating these systems, that split is the practical lesson. Treat the verifiable artifact and the unverifiable workflow as separate claims. A frontier model contributing a genuine, novel step in research mathematics is now demonstrated . A repeatable, autonomous discovery engine you could deploy is not — at least not from anything OpenAI has shown. Human framing and human verification remain load-bearing parts of the result, not ceremonial ones.
Sawin's Explicit n^1.014 and What That Exponent Means
Sawin's explicit bound is the number that turns a qualitative refutation into a measurable one: Princeton mathematician Will Sawin posted a companion paper (arXiv:2605.20579, submitted 20 May 2026 ) constructing arbitrarily large n-point planar sets with more than n1.014114 unit-distance pairs . OpenAI's manuscript had proved only existence — some absolute δ > 0 with ν(n) ≥ n1+δ for infinitely many n — without pinning down δ . Sawin's paper extracts a concrete, computable value from the same number-theoretic Golod–Shafarevich machinery, giving δ ≈ 0.014.
Modest as 0.014 looks, it is the first improvement to the lower-bound exponent in roughly 80 years . The significance is not the magnitude but the regime change. Erdős's near-linear conjecture allowed an exponent of the form 1 + O(1/log log n) — a quantity that converges to 1 as n grows, so the "extra" power over linear vanishes in the limit . A fixed δ behaves differently: n1.014 maintains a constant gap above the linear exponent for every sufficiently large n. Because any fixed positive δ eventually exceeds C/log log n for every fixed C, the two are not just different numbers — they describe qualitatively different growth.
The table below places the explicit bound against the long-standing landmarks. Note that the lower-bound and upper-bound exponents still bracket a wide interval; Sawin moved the floor, but the O(n4/3) ceiling proved by Spencer, Szemerédi, and Trotter in 1984 is untouched .
| Result | Type | Exponent on n | Year |
|---|---|---|---|
| Erdős grid construction | Lower bound | 1 + o(1) → 1 | 1946 |
| OpenAI model (existential) | Lower bound | 1 + δ, δ > 0 unspecified | 2026 |
| Sawin explicit | Lower bound | 1.014114 | May 2026 |
| Spencer–Szemerédi–Trotter | Upper bound | 4/3 ≈ 1.333 | 1984 |
For builders watching how AI output gets absorbed into mathematics, the sequence is the lesson: the model supplied an existential breakthrough, and a human mathematician — within days, using the same algebraic ingredients — quantified it into a checkable exponent . The gap between 1.014 and 1.333 remains open, and the exact asymptotic value of ν(n) is still unknown.
Lean Formalization and Proof Certification
No complete, independently certified Lean proof of the disproof exists yet. The Google DeepMind Formal Conjectures repository records Erdős Problem #90, the OpenAI disproof, the Alon et al. qualitative statement, and Sawin's explicit "1.014114" variant — but the visible theorem bodies still contain sorry placeholders, Lean's marker for an unproved goal . That makes the file a formal-statement benchmark, not machine-checked verification.
The distinction matters for anyone reading this as evidence of "AI-verified mathematics." What the Lean file certifies today is that the claims are stated precisely enough to be formalized — the conjecture, the existential lower bound, and the explicit exponent each have a typed signature. What it does not yet contain is a term that discharges those goals. Until the sorry tokens are replaced by checked proof terms, Lean is functioning as a problem-statement registry, not a certification layer .
Certification, for now, rests on human reading. The primary sources are three preprints outside conventional journal peer review: OpenAI's CDN-hosted manuscript, the digested arXiv note arXiv:2605.20695 by Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, and Wood, and Sawin's explicit-bound paper arXiv:2605.20579 — all dated 20 May 2026 . None has cleared journal review; the short human-verified note is what most mathematicians are treating as the trustworthy version of the argument.
The community ledger reflects this hybrid status. The Erdős Problems database now labels #90 "DISPROVED (LEAN)" and lists a $500 prize; its text notes Erdős offered $300 in 1982 for a proof or disproof of the n^(1+o(1)) form . The "(LEAN)" tag signals a formal statement on record, not a formal proof — a useful reminder that the disproof is verified by expert human reading, with full formalization still outstanding.
Interpreting the Result: AI Strengths and Boundaries in Hard Mathematics
The honest read on this result is that it plays directly to two properties frontier reasoning models already have — breadth across disparate subfields and tolerance for grinding through many failed attempts — and exposes the parts that still depend entirely on humans. The genuine advance was connecting algebraic number theory (class field towers, completely split primes, Minkowski lattices) to planar incidence geometry, a bridge no human had built in roughly 80 years . Analyst Timothy B. Lee framed it precisely: the AI's edge is searching widely across tools from unrelated areas and persisting through a "grind" of dead ends — Jacob Tsimerman reportedly tried a similar number-theoretic line and abandoned it as too time-consuming .
For practitioners, the limits are sharp and worth stating plainly:
- No reproducible path. The internal model is unnamed in the primary manuscript, and OpenAI disclosed no training details, sampling protocol, grading-pipeline specifics, or compute cost . There is no API or product you can route a conjecture through today to repeat this — claims tying the result to GPT-5, o3, or ChatGPT are unsupported by the sources.
- Humans framed the problem. The model received an AI-written problem statement; it did not autonomously decide which 1946 conjecture was worth attacking .
- Humans certified the proof. Mathematicians including Noga Alon, W. T. Gowers, Will Sawin, and Melanie Matchett Wood verified, rewrote, and simplified the argument; Sawin separately extracted the explicit n1.014 bound . The grading pipeline flagged confidence, but it did not produce a publication-ready paper.
That division of labor is the correct frame: human–AI collaboration, not end-to-end autonomous invention. Tim Gowers called the solution "a milestone in AI mathematics," and Daniel Litt described it as the first AI-produced result he found "exciting in itself" — both notable precisely because the bar for "genuinely new" was met, while neither claimed the verification step had become optional.
The concrete takeaway for builders: a frontier reasoning model contributed a verifiable, novel step in research mathematics — a δ ≈ 0.014 lower-bound improvement, the first in about 80 years . But it did so inside a human scaffold that chose the target and checked the output. If you are evaluating AI for hard technical work, the lesson is to pair it with experts for framing and certification, treat unreproducible vendor demos as exactly that, and measure value in verified steps — not in autonomy claims.
Frequently asked questions
Did the AI solve the unit-distance problem?
No. The model disproved Erdős's conjectured near-linear upper bound by constructing planar point sets with at least n1+δ unit-distance pairs for a fixed δ > 0, for infinitely many n . The exact asymptotic of ν(n) is still unknown, and the O(n4/3) upper bound proved by Spencer, Szemerédi, and Trotter in 1984 is untouched . "Disproved a conjecture," not "solved the problem," is the accurate framing.
Which OpenAI model produced the proof?
OpenAI has not named it. The primary manuscript describes only an "internal general-purpose reasoning model" and discloses no training details, sampling protocol, or compute cost . No production release — GPT-5, o3, or ChatGPT — is identified in any primary source, so claims tying the result to a specific named product are unsupported .
What does the n^1.014 exponent actually mean?
It is the first improvement to the unit-distance lower-bound exponent in roughly 80 years. Princeton's Will Sawin posted an explicit construction (arXiv:2605.20579, submitted 20 May 2026) giving n-point planar sets with more than n1.014114 unit-distance pairs . Previous constructions had an exponent that converged to 1 as n grew (n1+c/log log n); a fixed exponent above 1 is qualitatively different — its advantage compounds as point sets get larger .
Is the proof formally verified in Lean or peer-reviewed?
Neither, yet. Google DeepMind's Formal Conjectures repository records Problem #90, the disproof, and Sawin's explicit "1.014114" variant, but the visible theorem bodies contain sorry placeholders — a formal-statement benchmark, not a certified, independently checkable proof . The result currently exists as arXiv preprints and an OpenAI manuscript, none of which have completed conventional journal peer review . The Erdős Problems database labels Problem #90 "DISPROVED (LEAN)" and lists a $500 prize .
What does this mean for using reasoning models on hard research problems today?
Frontier reasoning models can make genuinely novel, verifiable contributions to mathematics when paired with expert human framing and post-hoc checking — but end-to-end autonomous proof discovery is not the current state. This result still required humans to set up the problem, verify the output, and simplify and strengthen the AI's argument before publication; a companion arXiv note by Alon, Gowers, Sawin, Tsimerman, Wood, and others (arXiv:2605.20695) supplied the digested, human-verified version . For builders, value is best measured in verified steps, not autonomy claims .
