openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance
← Problems

Discrete geometry · Combinatorics · Conjecture

Erdős unit-distance problem

Is the maximum number of unit-distance pairs among n distinct planar points bounded by n1+o(1)n^{1+o(1)} as n grows?

DisprovedOpenMath assessment · Oct 13, 2026
Frontier 5 reports →
Cite & export
Open this versionExport record · JSONRecord detailsReport a correction
Use with an agent

Overview

Known

A fixed positive power gain refutes the near-linear Euclidean conjecture in the cited proof and human companion exposition. Exact extremal growth remains a related research question.

Latest

Precise statement

Count unordered pairs of distinct points in the Euclidean plane at distance exactly one. Write u(n) for the maximum over all n-point sets. The conjecture asks that for every ε > 0, u(n) ≤ n^(1+ε) for all sufficiently large n. Determining the exact extremal growth remains a broader question.

Definitions

Unit-distance pair
An unordered pair of distinct planar points at Euclidean distance one. The extremal function counts the largest possible number of such pairs.

Question paraphrased by OpenMath. Original wording is available in the sources.

Landscape

Figures and explorable examples. Selecting a statement opens its exact wording.

Where the growth exponent lies

The true exponent θ is now known to lie strictly above 1 and at most 4/3. The 2026 gain δ is not explicit, so the open interval is drawn from 1, which is itself excluded. Erdős’s grid gives a gain c/log log n that tends to zero, which is why the conjecture θ = 1 was plausible.

11.11.24/3exponent θOpenthe true exponent, now known toexceed 1Targetθ = 1, Erdős’s conjecture, refutedProvedθ ≤ 4/3(Spencer–Szemerédi–Trotter)

Dataset erdos-unit-distance-exponent v1 · No computation: the interval endpoints 1 and 4/3 come from the cited statements. δ is not explicit in the sources, so no lower edge above 1 is drawn. Software: python 3.12.15. Exact rationals, stored as floating point. SHA-256 632e069fb580… · Download JSON

Data
LayerStatus
Open: the true exponent, now known to exceed 1open
Target: θ = 1, Erdős’s conjecture, refutedtarget
Proved: θ ≤ 4/3 (Spencer–Szemerédi–Trotter)proved

Visual setup

What counts as one unit-distance pair?

A unit square has four distance-one pairs; its diagonals are longer. Each unordered pair is counted once.

Reading boundary. A drawing of four points does not demonstrate a fixed exponent gain or the asymptotic counterexample.

What counts as one unit-distance pair?Four corner points form a square with its four sides highlighted. A dashed diagonal is excluded from the unit-pair count. This finite example introduces the quantity used in the asymptotic theorem.Distance 1√24 points · 4 unit pairs
Counting convention: unordered pairsQuestion scopeThe 2026 counterexample● Proved under stated assumptions

Four corners give four unit pairs; the diagonals have length √2 and do not count.

Text version

Four corner points form a square with its four sides highlighted. A dashed diagonal is excluded from the unit-pair count. This finite example introduces the quantity used in the asymptotic theorem.

The mathematical example is a unit square; the drawing coordinates are illustrative. Only distinct unordered Euclidean distance-one pairs count.

  1. Counting convention: unordered pairs

    Disproved

    The near-linear unit-distance conjecture

    The near-linear asymptotic assertion is refuted; this does not determine the exact maximum.

    The near-linear unit-distance conjecture →

  2. The 2026 counterexample

    Proved

    A fixed power gain for infinitely many sizes

    An asymptotic construction, not a statement about every size or an explicit value of δ.

    A fixed power gain for infinitely many sizes →

Sources & review

Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Results

The question 1

Counterexamples 1

Related advances 2

  • Proved
    The classical upper bound

    The classical incidence bound limits all finite point sets.

    Spencer, Szemerédi & Trotter 1984 · per Alon et al. 2026
  • Proved
    Erdős’s grid lower bound

    A lower bound for every large n from a scaled square grid; its exponent gain vanishes as n grows, unlike the 2026 fixed gain δ.

    Erdős · per Alon et al. 2026

Connections

Consequences 1

Assuming A fixed power gain for infinitely many sizesProved

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

Arithmetic creates many unit-length differences

The argument uses growing number fields, norm-one elements and a lattice window to create many planar distance-one pairs.

Cannot yet reach The four-point illustration is not the arithmetic construction or its proof.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Timeline

  1. A pinned Euclidean Lean submissionFormalization

    The repository supplies an exact theorem for the fixed exponent gain.

    The revision date is not the discovery date; OpenMath has not built the project.

  2. Erdős problem #90Formalization

    Formalization of an existing proof. Contribution type: Formalization.

    Open the Frontier report →

  3. Erdős problem #90New proof

    Full solution. Contribution type: AI standalone.

    Open the Frontier report →

  4. A model-generated construction refutes near-linear growthRelated result

    OpenAI releases the proof with a human companion argument.

    Discovery, exposition and later numerical exponent improvements have different credits.

    Also on the Frontier: Erdős problem #90 · Erdős unit-distance conjecture · Erdős problem #90

  5. A universal four-thirds upper boundBound established

    Spencer, Szemerédi and Trotter establish the classical incidence estimate.

    An upper bound does not exhibit configurations attaining it.

  6. Erdős introduces the planar distance questionFoundation

    The original point-pair question has an elementary formulation but an asymptotic target.

    Unit distances and distinct distances are different extremal questions.

Full history with sources →

Evidence

Literature

2 preprints · 3 projects

Status OpenMath assessment · Oct 13, 2026.

Formal

1 complete proof

1 formalization below ↓

Reported in sources: A pinned Lean submission reports the asymptotic counterexample with exact Euclidean pair counting. External execution and independent OpenMath review remain pending.

Computation

None recorded

Review

Not yet reviewed

OpenMath assessment: A fixed positive power gain refutes the near-linear Euclidean conjecture in the cited proof and human companion exposition. Exact extremal growth remains a related research question.

Source comparison and reader curation; independent mathematical assessment remains pending.

OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027

Collection last checked Oct 13, 2026.

Formalizations

A fixed power gain for infinitely many sizes →

Lean: positive exponent in the Euclidean planeComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

The finite-set definition counts ordered off-diagonal distance-one pairs and divides by two. The formal theorem uses EuclideanSpace ℝ (Fin 2), not the product sup norm, and proves arbitrarily large sizes. It does not specify δ = 0.014.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision
Submission.erdos_unit_distance_conjecture_false

Commit 2062b0e6c9770c81e397bfe41148e90b92ca0567

External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Bibliography 5

Research activity · 1 entry

Selected literature; source observations and coverage limits are retained in the publication details.

Contributors

OpenAI’s unnamed internal model generated the original construction. The nine companion-paper authors provide human exposition and checking; Will Sawin’s announced exponent refinement has separate credit. The plby/Erdos90 project supplies the linked formal submission; its checked README does not identify an individual formalization author.

Authors & roles

Remarks on the Disproof of the Unit Distance Conjecture →

Noga Alon · Thomas F. Bloom · W. T. Gowers · Daniel Litt · Will Sawin · Arul Shankar · Jacob Tsimerman · Victor Wang · Melanie Matchett Wood

The mathematical starting point is attributed to OpenAI’s model; the nine named authors supply exposition, checking, simplification and context.

OpenAI unit-distance announcement →

OpenAI

An unnamed internal model is credited for discovery. The announcement identifies external mathematicians; it does not make them the authors of the original AI argument.

These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.

Record details
Record version
6
Classification
MSC2020 52C10 / 05D99
Prerequisite level
undergraduate
Source observations & version history →