The higher-dimensional Erdős distinct-distances conjecture
The higher-dimensional Erdős distinct-distances conjecture is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). Erdős conjectured that for fixed dimension d ≥ 3, every set of n points in ℝd determines at least a constant times n2/d distinct distances, the order attained by the integer grid. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. For every fixed integer d ≥ 3, every set of n ≥ 2 distinct points in ℝd determines at least cdn2/d distinct distances, where cd > 0 depends only on d; the manuscript states that this resolves the higher-dimensional distinct-distances conjecture. Source: the manuscript The higher-dimensional Erdős distinct-distances conjecture, dated 23 September 2026.
- Formalization. The collection's index (commit
adc7f12) lists no Lean formalization for this family.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
2026-10-10 (latest commit eb37585, 14 October 2026) |
Yao Xu, cadamcat/distinct-distances-lean4 (GitHub) | Formalization (Lean) | A Lean 4 proof that for each d ≥ 3 there are constants 0 < c and 0 < C such that every finite set of at least two points in Euclidean d-space determines at least c · n2/d distinct distances, and that for every n ≥ 2 some n-point set determines at most C · n2/d. The README states that the formal proof follows the manuscript, that OpenAI's Lean library supplies a polynomial isolation interface, and that the distance definitions are copied from Google DeepMind's Formal Conjectures. The repository's history records a Comparator check of version 1.0.0 with two kernels. | Author-reported; the README states that the work was developed with AI assistance, and the attribution file states that the repository formalizes the theorem and does not claim a new mathematical solution. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.