---

Claim. No five-coloring of the edges of $K_{26}$ has every six vertices seeing all five colors; with the affine-plane coloring of $K_{25}$ this gives $N(5)=25$ in the repository's notation: the case $r=5$ of Problem 617. The source is the repository nwinter/erdos-617-r5 (history from 2026-07-12; pinned at its commit of 2026-08-01) with a write-up and the Lean 4 development lean617, posted to the site's proof-claim tab on 2026-07-31 by Nick Winter as a belated claim (the page's date; the repository's README dates its kernel-pure migration round to 2026-07-14). By the README, the final theorem erdos_617_r5_unconditional : Main is free of sorry and of mathematical hypotheses, and the file Statements.lean proves main_imp_upstream, that Main implies the formal-conjectures statement erdos_617 specialized to $r=5$ over an arbitrary $26$-element vertex type. The route: delete a vertex and partition the other $25$ by the color toward it; a hitter lemma forces five parts of five vertices carrying at most six own-color edges each, and a minority-color lemma forbids that. The Kang–Pikhurko (2005) equality classification of the extremal graphs at $(r,n)=(5,21)$ and Brouwer's 1981 Turán bound, on which the result was first conditional, are themselves proved in Lean. The trust base, as the README discloses, is the three standard axioms plus native_decide (Lean's ofReduceBool reflection) for four SAT certificates; the README says the whole development was authored by AI systems (the proof-claim entry names Claude Fable 5 and GPT-5.6 Sol) and reviewed only by other AI runs, not by human referees; the proof-claim entry adds that a second AI team's different proof of the case is included, which the repository holds, its provenance withheld, as review_queue/external-candidate-B.

Submission note. Posted to erdosproblems.com as a proof claim by Nick Winter (account nwinter) on 31 July 2026, giving "Claude Fable 5 and GPT-5.6 Sol" as the AI used:

Belated proof claim for the fixed r = 5 case: no 5-coloring of the edges of K₂₆ has every 6 vertices seeing all 5 colors. With the affine-plane coloring of K₂₅ this gives N(5) = 25. Route: delete a vertex and partition the other 25 by the color toward it. Then: 1) a hitter lemma forces five parts of five carrying at most six own-color edges each, but 2) a minority-color lemma forbids that. Originally, this relied on Brouwer's 1981 bound and the Kang–Pikhurko (2005) equality classification, but then it formalized those in Lean as well. A second AI team proved this case a different way; both proofs are included.

Covers. The fixed case $r=5$, with a Lean statement shown to imply the formal-conjectures statement at $r=5$.

Depends on. Nothing in this wiki.

Standing. Claimed. The corpus has not built this development, so it gives no formalized evidence; under the corpus's audit rule its native_decide dependence would count as a compiler axiom. No outside review is known; the site's label is FALSIFIABLE, and the claim carries no comments. The same case is claimed by Sneiderman (whose argument Kara formalized separately, as that page records), Silverstein and Rose. A partial claim derives nothing for the problem's standing.