---

Claim. Rafal Wrona submitted a full proof claim on the site's proof-claims thread for Problem 506 on 20 August 2026, pointing to a review manuscript and a Lean development in a public GitHub repository, linked above at the repository's commit of that day. The tab names the tools as OpenAI Codex, primarily GPT-5.6 Sol, with GPT-5.6 Terra and GPT-5.6 Luna for auxiliary and parallel work, and the repository's own account says that the mathematics, the manuscript, the checking scripts and the Lean source were developed with substantial AI assistance. The claimant is the human submitter. Write $f(n)$ for the least number of circles through at least three of $n$ points of the plane that are neither all collinear nor all concyclic. The claim is that

$$f(4)=3,\quad f(5)=5,\quad f(6)=8,\quad f(7)=11,\quad f(8)=17, \qquad\text{and}\qquad f(n)=1+\binom{n-1}{2}-\Bigl\lfloor\frac{n-1}{2}\Bigr\rfloor\ \ (n\ge9),$$

with explicit configurations attaining every value. The summary describes the method: each triple of points is assigned to the unique line or circle through it; inversion in a chosen point turns the circles through that point into lines of the inverted set, so that weighted bounds of Melchior and Langer type apply; estimates for rich lines and circles and a nonnegative weighted identity handle $n\ge15$, the case $n=14$ splits on whether a seven-point circle exists, and the cases $4\le n\le13$ use rigidity arguments and small explicit certificates. The formula from $n=9$ on agrees with the corrected Elliott bound, which Purdy and Smith assert for $n\ge394$, saying without printing it that Elliott's proof can be modified to give it; the values below $394$ are what that accepted partial result leaves open, and $f(8)=17$ is consistent with Segre's cube projection, which shows that eight points can determine fewer than $\binom{7}{2}=21$ circles. The repository also records two variants, under the hypotheses of no three collinear points and of no four concyclic points, which answer different questions and are not part of this claim.

Submission note. Posted to erdosproblems.com as a proof claim by Rafal Wrona (account rafalwrona) on 20 August 2026, giving "OpenAI Codex — primarily GPT-5.6 Sol, with GPT-5.6 Terra and GPT-5.6 Luna used for auxiliary and parallel work." as the AI used:

I claim the exact minimum number of proper circles determined by an $n$-point set that is neither collinear nor concyclic. The values are

$$> (f(4),f(5),f(6),f(7),f(8))=(3,5,8,11,17),$$

and for $n\ge9$,

$$> f(n)=1+\binom{n-1}{2}-\left\lfloor\frac{n-1}{2}\right\rfloor.$$

The proof

assigns every triple to its maximal line or circle. Inversion converts circles through a selected point into spanned lines, enabling weighted Melchior- and Langer-type bounds. Rich-carrier estimates and a nonnegative weighted identity handle $n\ge15$; $n=14$ is split according to the existence of a seven-point circle. Cases $4\le n\le13$ use projective rigidity and small explicit certificates. Explicit configurations establish sharpness. Notes: The repository also contains separate V3 and V4 formalizations. Under V3 (no three collinear points and not all concyclic), $f_{\mathrm{V3}}(8)=20$, while $f_{\mathrm{V3}}(n)=1+\binom{n-1}{2}$ otherwise. Under V4 (noncollinear and no four concyclic points), $f_{\mathrm{V4}}(n)=\binom{n-1}{2}$, with equality exactly for near-pencils. Conclusions remain separate between variants. Substantial AI assistance was used; independent human review is still being sought.

Formalization. The repository's formalization/Erdos506/Canonical.lean states Erdos506.erdos_506: for every n ≥ 4, the claimed value is the least k such that some Finset of n points of the plane, not Collinear and not Cospherical, has numCircles equal to k, where numCircles counts the spheres of the plane containing at least three of the points and is written to match the statement file of formal-conjectures for this problem. The README reports a build under Lean 4.30.0 with the pinned Mathlib and an axiom audit printing only propext, Classical.choice and Quot.sound, and says that the package is submitted for independent human review and is not a certificate of correctness. The file is a link and not formalized evidence, which requires Lean this corpus built and audited.

Depends on. No page of this wiki.

Acceptance. None documented. The manuscript is unpublished, the site's label and commentary are unchanged since 1 February 2026 and do not mention the claim, and the thread's one comment, of the same day, reports a shorter unpublished paper with the same result without naming or linking it, so it gets no page. The claim is therefore claimed, and the problem's standing follows it.