Proved
Fixed positive exponent gain proved ↗
For infinitely many n; unordered unit-distance pairs.
Planar Point Sets with Many Unit Distances · Theorem 1.1 and Statement on AI Use →
Source dated May 20, 2026 · Observed Oct 13, 2026
Theorem · version 2
A fixed power gain for infinitely many sizes
Statement
There exists such that for every N there are n ≥ N and a set of n distinct Euclidean planar points with at least unordered unit-distance pairs.
Assumptions
- Finite point sets in the Euclidean plane.
- The same δ works along an unbounded sequence of sizes.
Scope
An asymptotic construction, not a statement about every size or an explicit value of δ.
Evidence
Source reports
Proved
Formal exponent-gain endpoint reported complete ↗
Exact Euclidean norm and unordered counting; external proof execution.
Source dated Jun 27, 2026 · Observed Oct 13, 2026
Replaces an earlier source assessment. Version history ↓
Formal proofs
Lean: positive exponent in the Euclidean plane ↗
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_falseCommit 2062b0e6c9770c81e397bfe41148e90b92ca0567
Connections
In this problem · publication v4 · Selected context
Erdős unit-distance problem →
Counterexample · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v6
Erdős unit-distance problem →
Counterexample · Proved
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.
Unit-distance Lean submission ↗No OpenMath execution recorded
Exact proof source inspected. This digest identifies this file only, not a project build, theorem correspondence or independent reproduction.
Revision & attribution
Source revision: 2062b0e6c9770c81e397bfe41148e90b92ca0567. Observed Oct 13, 2026.
No specific AI contribution is attributed by this source record.
Unit-distance Lean submission: 2062b0e6c9770c81e397bfe41148e90b92ca0567.
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 · 2
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Formal exponent-gain endpoint reported complete ↗
Exact Euclidean norm and unordered counting; external proof execution.
Source dated Jun 27, 2026 · Observed Oct 13, 2026 · Source passage →
Replaces an earlier source assessment; see the original source for its history.
Proved
Fixed positive exponent gain proved ↗
For infinitely many n; unordered unit-distance pairs.
Source dated May 20, 2026 · Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-unit-distances-positive-exponent
- Statement version
- 2
- SHA-256
- 7fcef677de45cc684d0a81157257ec14a1347ff3720cf84c14f5eeeb95395fbd