---

Claim. No five-coloring of the edges of $K_{26}$ has all five colors on every six vertices, which the paper writes as $f(26,6,5)>5$ in the Erdős–Gyárfás notation: the case $r=5$ of Problem 617; with the coloring of $K_{25}$ from the affine plane of order five, $K_{25}$ is the largest complete graph with a balanced five-coloring, which the paper calls the sharp fixed-case threshold. This is Theorem 1 of Anthony Rose, A DRAT-certified proof of the Erdős–Gyárfás $r=5$ case, the file paper/erdos617_paper.md of the repository arose-logos/erdos-gyarfas-r5; the paper dates its core to 2026-06-09 and its revision to 2026-07-25, the repository's first commit is of 2026-07-24 (late UTC) and the posting to the site's proof-claim tab on 2026-07-25 is the first public posting, taken as the claim's date. The proof-claim entry names Codex and Claude as the systems used, and the paper credits them for computation and audit. The proof scales Lemma 2 of the 1999 Erdős–Gyárfás paper from $r=4$ to $r=5$: a least-used color has at most $65$ edges, independence number at most five and at most eleven edges on any six vertices; a three-vertex low-degree stripping argument with Brooks's theorem, Mantel's theorem and $R(3,5)=14$ reduces a counterexample to finitely many small residue graphs; a counting filter eliminates the larger residues (167.3 million candidates, none surviving); and the remaining $458$ SAT instances are all unsatisfiable, each verdict certified by a DRAT proof checked by drat-trim. The paper makes no priority claim, names the earlier claims of Sneiderman and Silverstein and Kara's formalization of Sneiderman's argument, and says the all-$r$ problem remains open.

Submission note. Posted to erdosproblems.com as a proof claim by Anthony Rose (account arose) on 25 July 2026, giving "Codex + Claude" as the AI used:

This is an additional independent proof (following two recent posts related to this) of the fixed $r=5$ case of Erdős Problem #617. We assume a counterexample and consider a least-used color. Its color graph has at most 65 edges, independence number at most five, and at most 11 edges on any six vertices. A three-vertex low-degree stripping argument, using Brooks’ theorem, Mantel’s theorem, and $R(3,5)=14$, reduces the problem to finitely many small residue graphs & a counting argument eliminates the larger residues. The remaining cases form an exhaustively generated collection of 458 SAT instances, all unsatisfiable, with each result certified by a DRAT proof checked using drat-trim. Together with the standard affine-plane coloring of $K_{25}$, this gives the sharp threshold for the fixed $r=5$ case. Notes: Obviously we've seen some progress on this in just the past week but I figured it may still be useful to post, as we have a different strip-and-residue reduction, 458 DRAT-verified SAT leaves, a 167.3-million-candidate density filter, and a release gate that regenerates the case tree from the structural specification.

Covers. The fixed case $r=5$ only.

Depends on. Nothing in this wiki.

Standing. Claimed. Unrefereed and computer-assisted; the artifact's manifest and release gate are the author's own; the site's label is FALSIFIABLE. The claim's one comment (Nick Winter, 31 July 2026) reports a review by their GPT-5.6 Sol and Claude Fable 5 agents at skim depth: the $458$-leaf case tree regenerated from the paper's structural rules independently of the author's scripts and matching the manifest exactly, with fifteen sampled leaves re-certified, two suggested simplifications, and the caveat that the replay used the same checker (drat-trim) as the author; it disclaims correctness and names no human referee, so it is no acceptance evidence. The same case is claimed by Sneiderman, Silverstein and Winter. A partial claim derives nothing for the problem's standing.