Proved
Classical 4/3 upper bound ↗
Historical universal upper bound; not a claim of optimality.
Remarks on the Disproof of the Unit Distance Conjecture · Theorem 1.1; Sections 1.1–1.3 and 2 →
Observed Oct 13, 2026
Bound · version 1
The classical upper bound
Earlier version 1. View current version 2 →
Statement
There exists C > 0 such that every n-point set in the Euclidean plane determines at most 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 v4 · 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.
In this problem · publication v5
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 →
- 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 →
- src/submission/Submission.lean; ChallengeDeps.lean pair-count definition → · Original passage ↗
Recorded wording
The pinned submission proves a positive exponent gain for arbitrarily large finite Euclidean planar point sets.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
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.
Proved
Classical 4/3 upper bound ↗
Historical universal upper bound; not a claim of optimality.
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-unit-distances-four-thirds-upper
- Statement version
- 1
- SHA-256
- 79a973c676012589c68193b5498be5e6ca7a463692055094c6ff98edd232bafd