Selected research history · publication v1

Erdős unit-distance problem

Follow the ideas, results and limitations over time. This is a selected history, not a complete literature survey or a measure of how close the problem is to being solved.

Current state & remaining question →

Viewing the timeline from pinned publication v1.

4 selected milestones · Source coverage checked 2026-10-13 · Historical annotation and mathematical review remain separate.

1946 publication
Foundation
Erdős introduces the planar distance question
The original point-pair question has an elementary formulation but an asymptotic target.
Scope & review: Unit distances and distinct distances are different extremal questions.
Statements & sources
- Erdős problem 90: unit distances ↗Problem 90; historical question and background
- Planar Point Sets with Many Unit Distances ↗Theorem 1.1 and Statement on AI Use
- Remarks on the Disproof of the Unit Distance Conjecture ↗Theorem 1.1; Sections 1.1–1.3 and 2
Historical annotation review: pending. The date refers to the publication, with the precision supported by the source.
1984 publication
Bound established
A universal four-thirds upper bound
Spencer, Szemerédi and Trotter establish the classical incidence estimate.
Scope & review: An upper bound does not exhibit configurations attaining it.
Statements & sources
- The classical upper bound →
- Remarks on the Disproof of the Unit Distance Conjecture ↗Theorem 1.1; Sections 1.1–1.3 and 2
Historical annotation review: pending. The date refers to the publication, with the precision supported by the source.
May 20, 2026 announcement
Related result
A model-generated construction refutes near-linear growth
OpenAI releases the proof with a human companion argument.
Scope & review: Discovery, exposition and later numerical exponent improvements have different credits.
Statements & sources
- A fixed power gain for infinitely many sizes →
- Planar Point Sets with Many Unit Distances ↗Theorem 1.1 and Statement on AI Use
- Remarks on the Disproof of the Unit Distance Conjecture ↗Theorem 1.1; Sections 1.1–1.3 and 2
- OpenAI unit-distance announcement ↗The unit distance problem; mathematicians on the result
Historical annotation review: pending. The date refers to the announcement, with the precision supported by the source.
Jun 27, 2026 formalization
Formalization
A pinned Euclidean Lean submission
The repository supplies an exact theorem for the fixed exponent gain.
Scope & review: The revision date is not the discovery date; OpenMath has not built the project.
Statements & sources
- A fixed power gain for infinitely many sizes →
- Unit-distance counterexample in Lean ↗src/submission/Submission.lean; ChallengeDeps.lean pair-count definition
Historical annotation review: pending. The date refers to the formalization, with the precision supported by the source.

← Back to the Problem

Erdős introduces the planar distance question

A universal four-thirds upper bound

A model-generated construction refutes near-linear growth

A pinned Euclidean Lean submission