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 2
The classical upper bound
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 v6
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 →
- 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
- 2
- SHA-256
- aa185865e54aa65983faa8d5c071c4e26c0c8ac30f3318ddee7ebfbee2394f5a