---

Claim. The answer to Problem 958 is no, by a single configuration. The four points $(0,0)$, $(1,0)$, $(0,1)$ and $(0,-1)$ determine the distances $1$, $\sqrt2$ and $2$, realized by $3$, $2$ and $1$ unordered pairs, so $k=3=n-1$ and $\{f(d_i)\}=\{3,2,1\}$; three of the points are collinear and the fourth is not, so the set is neither equally spaced on a line nor equally spaced on a circle. The "only if" direction of the question therefore fails at $n=4$. The set is a right isosceles triangle, $(1,0)$, $(0,1)$, $(0,-1)$, with its circumcenter $(0,0)$: an instance of the $n=4$ configuration Erdős himself gave in 1984, the vertices of an isosceles triangle with the center of its circumscribed circle ([Er84c, p. 135] on the problem page), so the example was in print before this posting, which proved it in Lean. The posting opens with a priority note citing the Seed-Prover 1.5 report of 19 December 2025, which lists Problem 958 among the problems that system solved without releasing the proof.

Claimant. Boris Alexeev posted the example on the site's discussion thread on 27 December 2025, writing that Aristotle (Harmonic) had found it by itself, and added the Lean proof to Alexeev's repository of formalized Erdős problems the same day; the file, linked above at a pinned commit, names Aristotle and Alexeev as formal authors and no informal author. Its theorem Erdos958.not_erdos_958 negates the statement that for every finite planar set $A$, the profile ($|D|=|A|-1$ and the multiplicities of the distances in $D$ form $\{1,\ldots,|A|-1\}$) holds exactly when $A$ is an arithmetic progression of points or the image of an arithmetic progression of angles on a circle; the multiplicities count unordered pairs of distinct points, and the file prints its axioms as propext, Classical.choice and Quot.sound.

Standing. The site's label carries a Lean marker and the curator credits the disproof to Clemen, Dumitrescu and Liu, whose accepted claim page gives a family of counterexamples of every size $n\geq4$. This corpus has not built or audited the Lean file, so no evidence is listed and the claim stays pending; the problem's standing rests on the accepted claim. The example refutes the corrected Statement of the problem page, which asks for the profile of every finite set with multiplicities counted over unordered pairs, as the Lean file counts them. The formal-conjectures statement file, linked above at a pinned revision, asks the question for all sufficiently large $n$ and names this set as a small exception; that question, and Erdős's own for $n>4$, are answered by the family of Clemen, Dumitrescu and Liu, not by this set, as the problem page records.