---

Claim. The paper A machine-checked proof that $n_4=7$ for Erdős problem #827 proves, as its Theorem 1, that every seven points of the plane in general position, pairwise distinct with no three collinear and no four concyclic, contain four points whose four triangles have pairwise different circumradii, and that some six points in general position do not. So $n_4=7$ for Problem 827. The lower bound is the set $\{\pm(1,0),\pm(1,1),\pm(2,3)\}$. For the upper bound the paper classifies the patterns of equal circumradii that a bad six-point set can carry, a bad set being one whose every four-point subset has two triangles of equal circumradius. Up to relabeling there are 35 classes, 34 of them are not realizable in general position, and the last forces the six points to be symmetric about a point. Seven points cannot have all their six-point subsets symmetric about a point without three collinear points. The Lean 4 theorem DistinctCircumradii.sInf_isGood_eq_seven states $\inf\{N:\text{IsGood }N\}=7$, and the paper reports that its axioms are only propext, Classical.choice and Quot.sound.

Submission note. Posted to the site's forum by Kiichi on 24 September 2026:

Re: exact value at k=4

We have an independent, machine-checked proof of n_4 = 7 (same convention: no three collinear, no four concyclic). The route is different from the one above: the upper bound goes through a certified enumeration of the 35 combinatorial types of "bad" six-point sets (the search tree and its pruning rules are proved sound inside the proof assistant), and the non-realisability of 34 of them is checked from explicit algebraic certificates rather than by a SAT solver or a computer algebra system. The remaining type forces the six points to be centrally symmetric (the same family as the lower-bound example above), and a seventh point then always completes a good quadruple. Everything, from the lower-bound configuration to the final statement 'sInf {N | IsGood N} = 7', is verified in Lean 4 with Mathlib; '#print axioms' reports only 'propext', 'Classical.choice', 'Quot.sound'. We did not re-run or audit the SAT/Singular computation above; this is a separate proof of the same value, which we hope serves as the independent check requested there.

Write-up: https://computoergosum.com/en/principia/erdos-827-n4.html Paper (with the correspondence between the paper's lemmas and the Lean declarations): https://computoergosum.com/principia/papers/erdos827-distinct-circumradii.pdf Lean sources and axiom logs: https://computoergosum.com/principia/lean/principia-src.tar.gz (sha256 131d8da3426838ca717991bf642551ee8fa5e2656c4952fb1babf050bd175c1b; the main theorem is 'DistinctCircumradii.sInf_isGood_eq_seven' in 'Principia/DistinctCircumradii/Final.lean')

Covers. The value $n_4=7$ under the problem's convention, and nothing for $k\ge5$ or for the growth of $n_k$.

Authors and AI use. The paper's authors are Kiichi, Shiori and Rin. Section 11 states that Shiori and Rin are instances of Claude (Anthropic), run as the coding agent Claude Code with models of the Opus 5 and Fable 5 series. Shiori produced the informal proof, the searches and the Lean development, and Rin rebuilt the development from the distributed archive. Kiichi, the human author, set the task and posted the result, and the paper says that Kiichi has not personally verified the mathematics.

Standing. Claimed. The proof was posted on the site's thread on 24 September 2026, and the paper is dated 3 October 2026. The paper credits the value to sallerk's computer-assisted proof of 22 September 2026 and offers its own as an independent route. The paper says that adversarial review was done only by further instances of the same model family and that no mathematician outside the authors has reviewed the work. This corpus has not built or audited the Lean development, so it is no formalized evidence.