Erdős Problem #958

Aristotle found a new proof of a problem that was already solved (27 Dec 2025).

Problem
Erdős problem #958 (distances, geometry); current status: disproved (Lean)
Credit
Aristotle · AI building on known literature
Checked
Lean formalizationListed in Tao's wiki
Timeline
First AI contribution 2025-12-27 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
PRIOR
ART
Per Tao's AI-contributions wiki

The problem

Let A⊂R2A\subset \mathbb{R}^2 be a finite set of size nn, and let {d1,…,dk}\{d_1,\ldots,d_k\} be the set of distances determined by AA. Let f(d)f(d) be the multiplicity of dd, that is, the number of ordered pairs from AA of distance dd apart.

Is it true that k=n−1k=n-1 and {f(di)}={n−1,…,1}\{f(d_i)\}=\{n-1,\ldots,1\} if and only if AA is a set of equidistant points on a line or a circle?

Statement quoted from erdosproblems.com/958, maintained by Thomas Bloom. Original source: [Er84c]. Current status there: disproved (Lean).

AI contributions

As recorded in Terence Tao's wiki AI contributions to Erdős problems (data as of 30 Jun 2026). 🟢 full, 🟡 partial, ⚪ unverified, 🔴 incorrect.

Date Kind AI systems Outcome Literature
27 Dec, 2025 AI building on known literature Aristotle 🟢 New proof found (Lean) 🟢 Clemen, Dumitrescu, and Liu (2025)

Caveats

The wiki's classifications are provisional and are not a benchmark. Many Erdős problems have never had a thorough literature review, so a result that looks new may later turn out to be known; some problems were also stated ambiguously or incorrectly. See the problem page for the full discussion.

∎