---

Claim. Under the general position of Problem 827, no three points on a line and no four on a circle, $n_4=7$. Call a set bad when each of its four-point subsets contains two triangles of equal circumradius. The lower bound $n_4\ge7$ comes from explicit bad six-point sets with integer coordinates, such as $(0,0),(0,7),(2,6),(4,3),(6,2),(6,9)$. They belong to a family of centrally symmetric sets $\{\pm u,\pm v,\pm w\}$ whose eight triangles taking one point from each pair share a circumradius. The upper bound rests on the fact that only two circles of a given radius pass through two points. Exact enumeration and a SAT search, with every surviving pattern refuted by ideal saturation in Singular over $\mathbb{Q}$, show that every bad six-point set is centrally symmetric. A count of the distinct pairwise sums then shows that no seven points can have all their six-point subsets centrally symmetric, so no bad seven-point set exists.

Covers. The value $n_4=7$ under the problem's convention. The write-up also records the lower bounds $n_5\ge9$, $n_6\ge11$ and $n_7\ge13$ from explicit witnesses, and the post adds $n_8\ge17$. Under the weaker convention of Martínez and Roldán-Pensado, which allows three points on a line, the argument gives only $7\le n_4\le9$, because the upper bound uses the absence of three collinear points. Nothing here bears on $n_5$ or on the growth of $n_k$.

Standing. Claimed. The proof was posted on the site's thread on 22 September 2026, with its write-up, witnesses and code in the linked repository, pinned at the commit of that day. The upper bound relies on a SAT solver and on Singular, and the author re-ran every computational step in a second implementation. The post discloses that the computations and the literature search were done with AI assistance, without naming a system, and calls the second run a re-check of the author's own work rather than an independent review. An independent proof of the same value by another route is the Lean-checked proof of Kiichi. No outside review is recorded. The claim was posted under the account sallerk, which shows no real name.