Erdős #90 — the unit distance conjecture (disproved 2026)

Statement

Does every set of $n$ distinct points in $\mathbb{R}^2$ contain at most $n^{1+O(1/\log\log n)}$ pairs which are at distance exactly $1$ apart? Erdős's associated conjecture (for which he offered the prize) is the weaker-looking upper bound $u(n)=n^{1+o(1)}$, where $u(n)$ is the maximum number of unit-distance pairs among $n$ planar points (erdosproblems.com/90). This conjecture is now FALSE (see Facts / Literature state).

Facts

- Prize \$500; status DISPROVED (LEAN) on erdosproblems.com/90 — "solved in the negative and the proof verified in Lean" (direct fetch 2026-07-21). Erdős's own offers were \$300 for a proof or disproof of $n^{1+o(1)}$ [Er82e] and \$250 in [Er83c]/[Er85]. - Falsifiable: not by a finite counterexample — the claim is asymptotic ($\forall$ large $n$); it was disproved instead by an *explicit infinite family* (a construction valid for infinitely many $n$). - Origin: Erdős, "On sets of distances of $n$ points," *Amer. Math. Monthly* 53 (1946) [Er46b]; Erdős dates the conjecture to 1946 in [Er94b]. Restated across [Er61] [Er75f] [Er81] [Er82e] [Er83c] [Er85] [Er90] [Er94b] [Er95] [Er97c] [Er97e] [Er97f] [Va99,4.67]. - Elementary bounds (classical). Every pair contributes to $\le 2$ circles, giving the trivial $u(n)=O(n^{3/2})$. Lower bound: the $\sqrt n\times\sqrt n$ integer grid realizes $u(n)\ge n^{1+c/\log\log n}$ (Erdős 1946 [Er46b]) — this is exactly why $n^{1+o(1)}$, *if true*, would be best possible; erdosproblems.com/90 states the optimality "is shown by a set of lattice points." - Best known UPPER bound: $O(n^{4/3})$, Spencer, Szemerédi, Trotter [SST84] (1984), unimproved in exponent for 40+ years — the point-vs-unit-circle incidence bound, see Incidence geometry: Szemerédi–Trotter theorem, the crossing lemma, and Zarankiewicz-type bounds. Valtr (see [Sz16]) built a metric on $\mathbb{R}^2$ with $\gg n^{4/3}$ unit pairs to which the SST84 proof still applies, so beating $n^{4/3}$ from above must exploit a *special feature of the Euclidean metric* (erdosproblems.com/90). This upper-bound side is untouched by the 2026 disproof. - DISPROOF (2026). For infinitely many $n$ there is a set $P$ of $n$ points in $\mathbb{R}^2$ with at least $n^{1+c}$ unit-distance pairs, $c>0$ an absolute constant (erdosproblems.com/90). Hence $u(n)\ne n^{1+o(1)}$: the true growth is *polynomially* above $n$. A short human-verified digest is Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, Wood, "Remarks on the disproof of the unit distance conjecture," arXiv:2605.20695 (20 May 2026); its abstract attributes the crucial ideas to Ellenberg–Venkatesh, Golod–Shafarevich, and Hajir–Maire–Ramakrishna. The construction was produced by an internal OpenAI model in May 2026 and verified/refined by those nine mathematicians and formalized in Lean (erdosproblems.com/90; arXiv:2605.20695 abstract) — a one-line provenance fact; the mathematics below is the substance. - Explicit exponent. Sawin, "An explicit lower bound for the unit distance problem," arXiv:2605.20579 (20 May 2026), abstract verbatim: "there are sets of $n$ points in the plane with $n$ arbitrarily large that contain more than $n^{1.014}$ pairs of points separated by a distance exactly $1$" — via constructing algebraic number fields with many primes of small norm through a Golod–Shafarevich criterion argument (Unbounded-degree number-field grids via infinite class-field towers (Golod–Shafarevich + point-counting)). Emmerich, arXiv:2606.03419 (2 Jun 2026), optimizes Sawin's parameters (prime set $T$, multiplicities $k(p)$, radius $R$) as a nonlinear integer program, certifying $u(n)>n^{1.0152}$ and $u(n)>n^{1.031}$; its references note concurrent community improvements past $n^{1.036}$. - Formalised in Lean: Yes (erdosproblems.com/90). Related OEIS: A186705. - Related problems (erdosproblems.com "See also"): [92], [96] (unit distances in a *convex* $n$-gon — is it $O(n)$?), [605], [956]; higher-dimensional generalisation [1085].

Literature state

Resolved (disproved). The conjecture $u(n)=n^{1+o(1)}$ — equivalently the $n^{1+O(1/\log\log n)}$ upper bound — is false. The break is entirely on the lower-bound side: an explicit algebraic construction forces $u(n)\ge n^{1+c}$ for an absolute $c>0$ (erdosproblems.com/90), and Sawin made it explicit at $n^{1.014}$ (arXiv:2605.20579), later pushed to $n^{1.0152}$–$n^{1.031}$ and beyond by parameter optimization (Emmerich, arXiv:2606.03419).

The mathematics that remains. The construction takes point sets built from the additive structure of the ring of integers $\mathcal{O}_K$ of a number field $K$ of large degree $d\asymp$ (a growing function of $n$): one needs $K$ with small root discriminant so that $\mathcal{O}_K$ embeds as a well-distributed lattice, and with many primes of small norm so that a single value (norm $=1$, i.e. a common "unit distance") is attained by unusually many pairs. Number fields with root discriminant bounded uniformly as the degree $\to\infty$ are exactly what infinite class field towers (Golod–Shafarevich criterion) and their tame refinements (Hajir–Maire–Ramakrishna) supply; the point-counting that turns "many small-norm primes in a small-discriminant field" into "many pairs at a common distance" is the Ellenberg–Venkatesh ingredient (arXiv:2605.20695 abstract; arXiv:2605.20579 abstract). This is why the disproof is a *construction*, not a search: the extremal configuration is dictated by deep arithmetic, and the naive grid (Erdős 1946) is provably not optimal.

What is still open. The upper bound remains $O(n^{4/3})$ (Spencer–Szemerédi–Trotter 1984 [SST84]); the 2026 work does not touch it. So the true exponent of $u(n)$ is now pinned only to the interval $[\,1.031\ldots,\ 4/3\,]$ (lower end rising as certificates improve, upper end static since 1984) — the actual order of magnitude of the maximum number of unit distances is wide open, and the Valtr metric obstruction (erdosproblems.com/90) shows any sub-$n^{4/3}$ upper bound must use Euclidean-specific rigidity — cf. Pach–Raz–Solymosi "Erdős's unit distance problem and rigidity" (arXiv:2507.15679, cited in wiki/problems/104.md).

Technique transfer (documented). This disproof directly inspired Bloom–Sawin–Schildkraut–Zhelezov to disprove the real-number sum-product conjecture by the same algebraic-integer machinery (arXiv:2605.28781, per wiki/problems/52.md) — the clearest documented case in this dataset of one Erdős problem's method Erdős #90 — the unit distance conjecture (disproved 2026) cracking another Erdős #52 — the sum-product problem for integers.

Attack surface

- Mode: resolved (literature-resolution complete) for the disproof; the live residual is derivation — closing the $[\,1.031\ldots,\,4/3\,]$ exponent gap. - Concrete next experiments: (1) push the explicit lower bound by re-running Emmerich's nonlinear-integer-program certificate search (arXiv:2606.03419) over larger prime sets / higher-degree towers — a directly runnable optimization with a mechanical Lean-checkable oracle; (2) attack the upper bound below $n^{4/3}$ by exploiting Euclidean rigidity in the SST84 point–unit-circle incidence argument, the direction flagged by Pach–Raz–Solymosi (arXiv:2507.15679) as reducing to a rigid-framework conjecture; (3) transfer the tower construction to sibling geometry problems — unit *circles* through 3 points Erdős #104 — o(n^2) unit circles through 3+ points (Elekes's 41-year-old $n^{3/2}$ bound never re-examined with these tools) and the convex-position case [96]. - Oracle: for the lower bound, a candidate point set (exact algebraic coordinates from $\mathcal{O}_K$) has its unit-distance count computed exactly and Lean-verified — this is *how the disproof itself was certified* (erdosproblems.com/90: "verified in Lean"); no finite oracle exists for the still-open upper-bound exponent. - Feasibility: the disproof is done and world-class; the tractable, high-value moves are the certificate-optimization lower bound (in reach, purely computational) and porting the construction to Erdős #104 — o(n^2) unit circles through 3+ points / [96], not the famous-and-hard $n^{4/3}$ upper bound.

Related

- [96] — unit distances among the vertices of a *convex* $n$-gon (is it $O(n)$?; erdosproblems.com/96, no page in this dataset); the convex-position sibling, best bound $n\log_2 n+4n$ (Aggarwal), still open — the rigid convex setting is where the tower construction does *not* obviously transfer. - Erdős #97 — convex polygon vertex with no 4 equidistant — convex polygon with no vertex seeing $\ge 4$ equidistant others; same "how many equal-distance incidences can a configuration force" family, and the page that flags Erdős #90 — the unit distance conjecture (disproved 2026) as the precedent that deep algebra beats naive/evolutionary search. - Erdős #104 — o(n^2) unit circles through 3+ points — $o(n^2)$ unit *circles* through $\ge 3$ points; closest sibling on the lower-bound side, where the same algebraic-number-theoretic construction is the main unexplored lever against Elekes's 1984 $n^{3/2}$ bound. - Erdős #52 — the sum-product problem for integers — sum-product for integers; the real-number analogue was disproved (arXiv:2605.28781) by explicitly importing *this* problem's number-field machinery — documented technique transfer. - Incidence geometry: Szemerédi–Trotter theorem, the crossing lemma, and Zarankiewicz-type bounds — Spencer–Szemerédi–Trotter's $O(n^{4/3})$ upper bound is a point-vs-unit-circle incidence bound; the still-open upper-bound side of #90 lives entirely here. - Unbounded-degree number-field grids via infinite class-field towers (Golod–Shafarevich + point-counting) — large-degree number fields of small root discriminant with many small-norm primes (Golod–Shafarevich class-field towers, Hajir–Maire–Ramakrishna tame towers, Ellenberg–Venkatesh point-counting); the construction that disproved #90 (arXiv:2605.20579) and, by transfer, the real sum-product conjecture. - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — the disproof is machine-checked (erdosproblems.com/90 status "DISPROVED (LEAN)"); the certificate-optimization lower bounds (arXiv:2606.03419) are of exactly the Lean-verifiable form.