この記事の日本語版はまだありません。英語版を表示しています。

Erdős Problem #958

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

問題
Erdős problem #958 (distances, geometry); current status: disproved (Lean)
貢献
Aristotle · AI building on known literature
検証
Lean formalizationListed in Tao's wiki
経緯
First AI contribution 2025-12-27 · wiki data as of 2026-06-30
出典
Problem page (erdosproblems.com)Tao's AI-contributions wiki
既知
文献
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.

∎