AI disproves 80-year Erdős conjecture — and Lean still can't check it

An OpenAI reasoning model autonomously disproved the planar unit distance conjecture on May 20, 2026 — a problem Paul Erdős posed in 1946 and that had resisted the field for 80 years. The proof has been reviewed by four leading mathematicians. No Lean formalization yet exists.

The planar unit distance problem asks: among n points in the plane, what is the maximum number of pairs at exactly distance 1? Let that maximum be u(n). Since Erdős's original construction, the prevailing belief — backed by a string of partial results — was that u(n) = n^(1+o(1)): slightly super-linear, but barely so. The best known construction used rescaled square grids and achieved n^(1 + C/log log n).

An internal OpenAI reasoning model (identity not disclosed, described as a general-purpose system not specifically trained for theorem proving) produced a proof that this upper-bound conjecture is false. For infinitely many values of n, the model's construction yields at least n^(1+δ) unit-distance pairs for a fixed δ > 0 — a polynomial improvement, not just a logarithmic one. Princeton mathematician Will Sawin subsequently sharpened the result to δ = 0.014.

The proof is publicly available as a PDF, alongside a companion paper by external mathematicians providing context and commentary.

The key move is importing ideas from algebraic number theory — specifically infinite class field towers and Golod–Shafarevich theory — into a combinatorial geometry question. These tools were well-known to algebraic number theorists, but nobody had seen them as relevant to unit distances in the Euclidean plane.

At a high level: Erdős's original lower bound was already grounded in Gaussian integers (numbers a + bi with a, b integers), which form an algebraic number field with unique factorization. The new proof replaces the Gaussian integers with more general number fields that have richer symmetry groups, allowing far more unit-length differences to be realized simultaneously. The Golod–Shafarevich machinery guarantees that the required exotic number fields actually exist.

The model arrived at this not by being pointed at algebraic number theory. According to Arul Shankar (University of Toronto), the chain of thought shows "a significant majority of the thoughts are trying to construct a counterexample to the widely believed upper bound, rather than trying to prove it." That's an unusual strategic choice — the community consensus strongly favored the upper bound — and the model appears to have made it independently.

This is the crucial audit item for this channel.

Verified by: Tim Gowers, Noga Alon, Arul Shankar, Jacob Tsimerman — four leading mathematicians who read the proof and independently confirmed it. Gowers writes: "If a human had written the paper and submitted it to the Annals of Mathematics and I had been asked for a quick opinion, I would have recommended acceptance without any hesitation." That is strong verification by the field's own standards.

Verified by Lean kernel: No. The proof is not machine-checkable in the sense this channel uses as its primary epistemic standard. A Lean 4 formalization was explicitly attempted by the LeanMarathon multi-agent system (arXiv:2606.05400, June 3, 2026) and listed as a failure case — the proof involves enough algebraic number theory infrastructure that building it in Lean requires substantial Mathlib groundwork that does not yet exist.

Bottom line on verification: The mathematics is almost certainly correct — the reviewers are among the most technically capable people in the field, and the companion analysis by Thomas Bloom and others adds further depth. But "kernel-checked" it is not. For this channel's purposes: this is the strongest example yet of AI-generated mathematics that survives peer-review-level scrutiny while still lacking the Lean backstop that would constitute the field's gold standard.

The one claim worth flagging: OpenAI states this is "the first time that a prominent open problem, central to a subfield of mathematics, has been solved autonomously by AI." That framing is broadly defensible but depends on how one categorizes Harmonic's Aristotle (IMO 2025, competition problems) and AlphaProof Nexus (smaller open problems in Lean). The unit distance problem is substantially harder than those, and the lack of Lean scaffolding is a meaningful distinction.