The Erdős Unit Distance Problem: Disproof and Exposition

An independent study project reconstructing and explaining the May 2026 disproof of Erdős's unit distance conjecture — the first prominent open problem in mathematics solved autonomously by AI.

The Problem

How many pairs of n points in the plane can be exactly distance 1 apart?

Let u(n) = max number of unit-distance pairs among n points in ℝ².

Bound	Source	Year
u(n) ≥ n^{1 + Ω(1/log log n)}	Erdős (square grid)	1946
u(n) ≤ O(n^{4/3})	Spencer, Szemerédi, Trotter	1984
u(n) ≥ n^{1+ε} (inexplicit ε)	OpenAI model	May 2026
u(n) ≥ n^{1.014}	Sawin (explicit)	May 2026
u(n) ≥ n^{1.03583...}	Naslund (MathOverflow, unverified)	May 2026

Erdős's Conjecture (1946): u(n) = n^{1+o(1)} — essentially linear.

Status: Disproven. There exist point sets with u(n) ≥ n^{1+δ} for a fixed δ > 0, infinitely often. The best verified explicit exponent is δ = 0.014 (Sawin).

The Proof in One Paragraph

The classical lower bound uses the Gaussian integers ℤ[i] (a number field with unique factorization) to construct lattice point sets. The key insight of the AI proof is to replace ℤ[i] with increasingly complex number fields from infinite class field towers of Golod-Shafarevich type. These are sequences of number fields Kⱼ of growing degree [Kⱼ:ℚ] → ∞ but bounded root discriminant. In each such field, the pigeonhole principle on ideal classes produces many algebraic numbers of complex absolute value 1. Embedding these fields into ℂ (via the Minkowski embedding) and taking a bounded window gives finite point sets in the plane. The unit-distance pairs come from translating lattice points by these "unit norm" elements. Because the number of unit-norm elements grows exponentially in the field degree while the denominator stays bounded (thanks to bounded root discriminant), the ratio of unit distances to points exceeds n^{1+δ} for a fixed δ > 0.

Key Ingredients

1. CM fields — totally imaginary quadratic extensions of totally real fields, where "absolute value 1 in one embedding ⟺ absolute value 1 in all embeddings."

2. Golod-Shafarevich theorem — gives conditions under which an infinite tower of number field extensions exists (specifically, when relations grow slower than the square of generators). This produces fields of unbounded degree but bounded root discriminant.

3. Pigeonhole on ideal classes — among ∏(kⱼ+1) ideals formed from split prime pairs, two must land in the same ideal class. Their ratio gives a unit-norm element with bounded denominator.

4. Geometry of numbers (Minkowski embedding) — embeds 𝒪_K as a lattice in ℂᶠ, enabling counting of lattice points in bounded regions.

Project Structure

erdos-unit-distance/
├── docs/
│   ├── proof.md              ← Full proof, self-contained
│   └── background.md         ← Mathematical prerequisites
├── src/
│   ├── count_unit_distances.py   ← Numerical verification on small cases
│   ├── gaussian_grid.py          ← Classical Erdős grid construction
│   └── class_field_tower.py      ← Sketch of Golod-Shafarevich conditions
├── references/
│   └── bibliography.md
├── notebooks/
│   └── exploration.ipynb
└── README.md (this file)

Sources

• Original AI proof: OpenAI announcement (May 20, 2026)
• Human-verified writeup: Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, Wood. Remarks on the disproof of the unit distance conjecture. arXiv:2605.20695
• Explicit exponent (δ=0.014): Sawin, Will. An explicit lower bound for the unit distance problem. arXiv:2605.20579
• Optimizer tracker: Erdős unit distance exponent (Tao's optimization problems page)

License

MIT — this is an educational reconstruction of publicly available mathematical results.