Let U(n) be the maximum number of unordered pairs of points at Euclidean distance 1 among any set of n points in the plane, that is, U(n)=max_P⊆R^2,,|P|=n#biglp,q⊆ P:|p-q|=1 bigr. The conjecture asks whether U(n)=n^1+o(1), equivalently, whether for every varepsilon>0 there exists n_0 such that U(n)≤ n^1+varepsilon for all n≥ n_0.

Erdős Problem 421

Let $U(n)$ be the maximum number of unordered pairs of points at Euclidean distance $1$ among any set of $n$ points in the plane, that is, $U(n)=\max_{P\subseteq\mathbb{R}^{2},\,|P|=n}\#\bigl\{\{p,q\}\subseteq P:\|p-q\|=1\bigr\}$ . The conjecture asks whether $U(n)=n^{1+o(1)}$ , equivalently, whether for every $\varepsilon>0$ there exists $n_{0}$ such that $U(n)\leq n^{1+\varepsilon}$ for all $n\geq n_{0}$ .

Sources & referencesView supporting material

Primary source

GitHub

Additional references

Erdős Problem 421 audit — GitHub

1 day ago

Progress summary

Refreshed 1 day ago

Solved

A construction checked by mathematicians and formal-verification work now establishes that Erdős Problem 421 is solved.

Erdős Problem 421 concerns the conjecture that $n$ planar points determine at most $n^{1+o(1)}$ pairs at unit distance. A construction with more such pairs disproves the conjecture.

May–August 2026 construction and verification

An internal OpenAI model produced a counterexample with at least $n^{1+\delta}$ unit-distance pairs for infinitely many $n$ ; Will Sawin refined it to $\delta=0.014$ . External mathematicians checked the argument, and a later audit expanded formal verification and strengthened the short-gap estimate. The available evidence supports closure, though the audit is a verification repository rather than journal confirmation.

Current status (as of August 2026): The conjecture is resolved by a publicly described counterexample, with external checking and expanded formal verification; no specific gap or retraction is reported.

Sources

No solutions have been posted yet.