---

Claim. The statement of Problem 655 as the site prints it is false. Let $X$ be the vertices of a regular $n$-gon. From a vertex, the other vertices lie at the distances $2\sin(\pi m/n)$ with $1\le m\le n-1$, and two of these coincide only for $m$ and $n-m$. So every circle centered at a vertex passes through at most two other vertices, and $X$ satisfies the hypothesis, while its distances are the $\lfloor n/2\rfloor$ values with $1\le m\le\lfloor n/2\rfloor$. Since $\lfloor n/2\rfloor<(1+c)n/2$ for every $c>0$ and every $n$, no constant $c>0$ works. The site's curator credits the observation to Zach Hunter in the problem's commentary and adds that some general-position hypothesis was presumably intended.

Later work. Przemek Chojecki's note Erdős Problem #655 and Its Natural Repairs: Exact Resolutions, Historical Sources, and Open Variants (ulam.ai, dated 22 April 2026, posted on the site's thread that day with the remark that GPT-5.4 Pro was used to trace the variants; source card) proves the matching lower bound: under the hypothesis every point sees at least $\lceil(n-1)/2\rceil=\lfloor n/2\rfloor$ distances, so the least number of distances is exactly $\lfloor n/2\rfloor$ (Theorem 3.1). Adding only no three points on a line, or only convex position, leaves the regular polygon admissible (Corollary 3.2 and Remark 3.3). The note also reports (Section 4.2) that Erdős, asking in 1988 whether some point sees more than $(1+c)n/2$ distances when no four points lie on a circle and every circle centered at a point holds at most two others, remarked that some cocircularity restriction is needed because the regular polygon is otherwise a counterexample. The note's exact minimum adds only the site's own easy bound to Hunter's polygon, so it is disclosed here and has no page of its own.

Formalization. Alper Ferudun's Lean file in Ferudun's fork of formal-conjectures, linked above at its pinned commit, says that it formalizes Hunter's observation and proves the printed statement false from the regular $n$-gon. The formal-conjectures catalog has recorded it as the formal proof of its erdos_655 since 22 June 2026, and the pull request that recorded it states that the proof uses no sorry and only the standard axioms. The corpus has not built or audited it, so it is a link here and not formalized evidence.

Depends on. No page of this wiki.

Standing. Claimed. The observation is unrefereed, and the site labels the problem OPEN, so its commentary is not acceptance and no reviewed evidence is listed. The formal-conjectures statement file states the printed question with the answer no, marks it solved, and states the general-position version as a separate open variant. The site's page shows no last-edited date; the observation is absent from the archived copy of the page of 21 July 2024 and present in the archived copy of 24 April 2025, the date this page carries.