Bound · version 2

The classical upper bound

Statement

There exists C > 0 such that every n-point set in the Euclidean plane determines at most Cn4/3Cn^{4/3} unordered unit-distance pairs.

Assumptions

  • Finite distinct planar points.
  • Unit distance uses the Euclidean norm.

Scope

Spencer–Szemerédi–Trotter’s classical bound; the optimal exponent remains a separate question.

Evidence

Source reports

Connections

In this problem · publication v6 · Selected context

Erdős unit-distance problem →

Related result · Proved

Scope: The classical incidence bound limits all finite point sets.

Limit: Determine the sharp growth between the counterexample construction and universal upper bounds.

Lower and upper estimates constrain the same extremal quantity in opposite directions.

Related results · 1

Relationship not independently reviewed. This concerns its use in this problem.

Sources

Planar Point Sets with Many Unit Distances →

  • Theorem 1.1 and Statement on AI Use → · Original passage ↗
    Recorded wording

    Theorem 1.1 constructs arbitrarily large planar sets with a fixed positive exponent gain in their unordered unit-distance count.

    paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.

OpenAI · Preprint · Publication date May 20, 2026

Revision & attribution

Source revision: 2026-05-20. Observed Oct 13, 2026.

The manuscript credits an internal OpenAI model with the original argument; subsequent human editing and external mathematical checking are separate roles.

Remarks on the Disproof of the Unit Distance Conjecture →

  • §1.1, History of the problem; §2 opening → · Original passage ↗
    Recorded wording

    Erdős showed with a √n × √n grid that n points can have n^(1+Ω(1/log log n)) unit distances, and conjectured an upper bound n^(1+o(1)). The best upper bound, O(n^(4/3)), is due to Spencer, Szemerédi and Trotter (1984).

    paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.

  • Theorem 1.1; Sections 1.1–1.3 and 2 → · Original passage ↗
    Recorded wording

    The companion paper provides a human-digested argument and background for the exponent gain, including the classical upper bound.

    paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.

Noga Alon · Thomas F. Bloom · W. T. Gowers · Daniel Litt · Will Sawin · Arul Shankar · Jacob Tsimerman · Victor Wang · Melanie Matchett Wood · Preprint · Publication date May 20, 2026

Revision & attribution

Source revision: 2026-05-20. Observed Oct 13, 2026.

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

Unit-distance counterexample in Lean →

plby/Erdos90 project · Project documentation · Publication date Jun 27, 2026

Public formal source; execution and statement correspondence are separate checks.

Revision & attribution

Source revision: 2062b0e6c9770c81e397bfe41148e90b92ca0567. Observed Oct 13, 2026.

No specific AI contribution is attributed by this source record.

History

Statement versions

Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.

Assessment history · 1

Assessments retained in these publication records. Earlier statement versions retain their own source histories.

Record details
Claim ID
claim-unit-distances-four-thirds-upper
Statement version
2
SHA-256
aa185865e54aa65983faa8d5c071c4e26c0c8ac30f3318ddee7ebfbee2394f5a

Publication records