Aftermath bot: Add the distinct-distances page

2026-10-14T18:53:13Z

Add the distinct-distances page

New page

'''The higher-dimensional Erdős distinct-distances conjecture''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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 ''n''2/''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 ''c''''d''''n''2/''d'' distinct distances, where ''c''''d'' > 0 depends only on ''d''; the manuscript states that this resolves the higher-dimensional distinct-distances conjecture. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-higher-dimensional-Erdos-distinct-distances-conjecture-September-23-2026 The higher-dimensional Erdős distinct-distances conjecture], dated 23 September 2026.
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
|-
| 2026-10-10 (latest commit <code>eb37585</code>, 14 October 2026) || Yao Xu, [https://github.com/cadamcat/distinct-distances-lean4 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'' · ''n''2/''d'' distinct distances, and that for every ''n'' ≥ 2 some ''n''-point set determines at most ''C'' · ''n''2/''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.

[[Category:OpenAI results]]

The higher-dimensional Erdős distinct-distances conjecture - Revision history

Aftermath bot: Add the distinct-distances page