Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 617

claims/: The 10 claim pages of Problem 617, one per claimant's result; the problem's standing derives from them.

Statement. Let $r\geq 3$ . If the edges of $K_{r^2+1}$ are $r$ -coloured then there exist $r+1$ vertices with at least one colour missing on the edges of the induced $K_{r+1}$ .

Status. Falsifiable, the site's label: a counterexample would be a finite coloring for one value of $r$ and could be checked by a finite computation, while a proof for every $r\ge3$ could not. The problem is open: the cases $r=3,4$ are refereed (Erdős and Gyárfás 1999, the accepted partial claim page 1999_04_01_erdos_gyarfas, and, for $r=3$ , earlier by Chung and Liu 1978 (1978_01_01_chung_liu)); the fixed cases $r=5,\ldots,11$ are claimed in 2026 preprints, write-ups and Lean developments recorded on the claim pages below, none refereed, and none with a review that counts as acceptance; and no proof for all $r\ge3$ and no counterexample is known (site accessed 2026-09-04; proof-claim thread with its comments and discussion thread accessed 2026-10-07). Partial claims derive nothing for the standing.

Source. erdosproblems.com/617, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #617, https://www.erdosproblems.com/617.

References.

[ErGy99] Erdős, Paul and Gyárfás, András, Split and balanced colorings of complete graphs. Discrete Math. 200 (1999), 79--86; doi:10.1016/S0012-365X(98)00323-9. Library home: erdos_gyarfas_1999_split_balanced_colorings_complete_graphs.

Formalization. Statement in formal-conjectures.

Current assessment

The site's falsifiable label is explained under Status. above.

The 1999 Erdős--Gyárfás paper [ErGy99] (refereed) proves the conjecture for $r=3$ (Lemma 1, pp. 84--85: every three-coloring of $K_{10}$ ) and $r=4$ (Lemma 2, pp. 85--86: every four-coloring of $K_{17}$ ), the accepted partial claim of 1999_04_01_erdos_gyarfas. A comment on the site's discussion thread (15 July 2026) reports that Chung and Liu, A generalization of Ramsey theory for graphs, Discrete Math. 21 (1978), no. 2, 117--127, doi:10.1016/0012-365X(78)90084-5, proved the $r=3$ case twenty-one years earlier as $R^3_2(K_4,K_4,K_4)=10$ , and points to Harborth and Möller (1999) and Munemasa and Shinohara (arXiv:1406.2050) on the weakened and complementary Ramsey numbers in which the problem's fixed cases live; the 1978 result is the accepted partial claim 1978_01_01_chung_liu. The fixed cases $r=5,\ldots,11$ are claimed in 2026 preprints and computational artifacts, each recorded as a claimed partial result on its own claim page under claims/. Each item below gives the source's own claim and its own audit or replay report; none is independently checked in this corpus:

[[../library/extremal_graph_theory/sneiderman_2026_five_color_case_balanced_coloring/_index|Sneiderman's $r=5$ preprint]] (unrefereed; claim page 2026_07_18_sneiderman_r5) claims to prove the fixed five-color case. Kara's 2026 artifact, a Lean and LRAT formalization of Sneiderman's argument for the exact fixed statement with its own axiom audit and a passing test suite, is the formalization link on that claim page. Three further independent proofs of the same case were posted to the site in July 2026 and have claim pages: Silverstein's one-color counting argument with twelve DRAT-certified formulas, Rose's strip-and-residue reduction to 458 DRAT-certified SAT instances, and Winter's Lean development, whose SAT certificates rest on native_decide.
[[../library/extremal_graph_theory/sneiderman_2026_six_color_case_balanced_coloring/_index|The $r=6$ preprint]] (unrefereed; claim page 2026_07_18_sneiderman_r6) claims to prove the fixed six-color case and reports that the argument survived an accompanying hostile review and 112 arithmetic and finite-classification checks; a Lean 4 formalization of this proof by Winter's AI agents (1 August 2026) is the formalization link on the claim page.
[[../library/extremal_graph_theory/sneiderman_2026_seven_eight_color_cases_balanced_coloring/_index|The $r=7,8$ preprint]] (unrefereed; claim page 2026_07_20_sneiderman_r7_r8) claims to prove the fixed seven- and eight-color cases and reports a replay of the complete $r=7$ enumeration and of every $r=8$ semantic reconstruction and LRAT certificate; a forum review of 31 July 2026 reports an inference gap shared with the $r=9$ manuscript, with a repair the linked version does not contain (claim page).
[[../library/extremal_graph_theory/sneiderman_2026_nine_color_case_balanced_coloring/_index|The $r=9$ preprint]] (unrefereed; claim page 2026_07_21_sneiderman_r9) claims to prove the fixed nine-color case and reports a full fixed-hash release replay with 332 reconstructed terminal cases, 50 CNFs, and 50 LRAT proofs; the same forum review reports the shared inference gap (claim page).
[[../library/extremal_graph_theory/codex_terpstra_2026_fixed_r10_r11_erdos_617/_index|The $r=10,11$ artifact]] (a preprint draft written by OpenAI Codex under Adam Lee Terpstra's direction, with a public computational artifact, unrefereed; claim page 2026_08_11_terpstra) claims to prove the fixed ten- and eleven-color cases through 48 outer comparisons for $r=10$ and 63 for $r=11$ , with no proof-assistant or SAT/LRAT certificate (source text, sections “r=10 evidence” and “r=11 evidence”); its repository reports two clean-room audits of its own, one of them as a retained r=10 audit manuscript.

In sum, the $r=3,4$ cases are refereed (Erdős--Gyárfás 1999; $r=3$ first by Chung--Liu 1978); the $r=5,\ldots,11$ cases rest on unrefereed 2026 preprints, write-ups and artifacts, each recorded as a claimed partial result on its claim page, with AI-assisted forum reviews and reproductions that limit or disclaim their verdicts and no review that counts as acceptance. These parameter-specific results do not settle the quantified assertion for all $r\geq3$ , so the full problem is open. Search scope: the site record (accessed 2026-09-04), its proof-claim thread with the comments on the claims and its discussion thread (accessed 2026-10-07), and the dated sources listed above; arXiv, citation indexes, author pages and X were not searched, so the date is not evidence that no further result exists. Another isolated positive case would extend the table but would not supply a route to the full problem; a uniform proof for infinitely many $r$ would be meaningful partial progress, while the target remains a proof for every $r$ or a rigorously verified counterexample.

Proof claims on the site. The site's proof-claim tab carries seven claims, all partial and all for fixed values of $r$ , posted between 18 and 31 July 2026: Sneiderman's four preprints for $r=5$ , $r=6$ , $r=7,8$ and $r=9$ (the library sources above), Silverstein's and Rose's computer-assisted proofs of $r=5$ , and Winter's Lean development for $r=5$ . Each has a claim page named above with its links, the claimant's own account of its checks and the standing claimed; Kara's formalization, not on the tab, is a link on Sneiderman's five-color page, and Terpstra's artifact, not on the tab either, has a claim page. The site's label is FALSIFIABLE (page last edited 1 April 2026). The comments on the claims (23 July to 1 August 2026) are forum users' AI-assisted reviews, reproductions and announcements, and the claimants' replies. None is by a named human referee, and the reviews limit or disclaim their verdicts; two comments announce self-declared Lean formalizations of Sneiderman's proofs (Kara's of $r=5$ , Winter's of $r=6$ ), and one announces an unposted independent proof of $r=5$ . They are recorded on the claim pages and give no acceptance evidence. The discussion thread holds two comments: a typo report and the 15 July 2026 priority report on Chung and Liu recorded above. The page's standing is derived from the claim pages, on which every claim is partial.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (87)

Chung and Liu prove the case r = 3 Erdős and Gyárfás prove the cases r = 3 and r = 4 Sneiderman's proof of the five-color case Sneiderman's proof of the six-color case Sneiderman's computer-assisted proofs of the seven- and eight-color cases Silverstein's computer-assisted proof of the five-color case Sneiderman's computer-assisted proof of the nine-color case Rose's DRAT-certified proof of the five-color case Winter's Lean-formalized five-color case Terpstra's computer-assisted ten- and eleven-color cases problems/extremal_graph_theory/E0617/claims Extremal and Structural Graph Theory The Ramsey Turnaround Numbers Split and balanced colorings of complete graphs On splittable colorings of graphs and hypergraphs Generalized Split Graphs and Ramsey Numbers Problems close to my heart A finite basis characterization of α-split colorings The Ramsey Turnaround Numbers Lemma 8.7 (p. 41): a projective plane of order r+1 gives a balanced (r,2)-coloring of K_{r^2+r+1}On the connection between chromatic number, maximal clique and minimal degree of a graph Theorem 1.1 (p. 207): a K_r-free graph with minimum degree above (3r-7)n/(3r-4) has chromatic number below r Codex–Terpstra: The fixed cases r=10 and r=11 of the Erdős–Gyárfás balanced-colouring conjecture Split and balanced colorings of complete graphs Conjecture 1 (p. 80): every r-coloring of K_{r^2+1} has r+1 vertices missing a color Construction (p. 80): affine planes give r-colorings of K_{r^2} with every r+1 vertices spanning all colors Lemma 1 (p. 84): every 3-coloring of K_10 has four vertices missing a color Lemma 2 (p. 85): every 4-coloring of K_17 has five vertices missing a color Proposition 2 (p. 84): g_3(2) = 13 Proposition 3 (p. 85): g_4(2) = 21 Theorem 5 (p. 83): f_r(2) ≤ g_r(2) ≤ r^2+r+1 if a projective plane of order r+1 exists Theorem 6 (p. 83): r^2 + 1 ≤ g_r(2)A proof of the stability of extremal graphs, Simonovits' stability from Szemerédi's regularity Corollary 2 (p. 3): a K_(p+1)-free graph with at least e(T_(n,p)) - t edges is within 3t edits of a complete p-partite graph Theorem 1 (p. 3): a K_(p+1)-free graph with e(T_(n,p)) - t edges loses at most t edges to become p-chromatic On splittable colorings of graphs and hypergraphs Theorem 1: an (r,v)-net with v > r(m-1) gives f_r(m) <= g_r(m) <= v^2 Theorem 10: g_r^k(k) = rk + 1 for r <= (k+1)/(4 ln(k+1))Theorem 11: f_r^k(k) >= rk + 1 for r >= 3 Theorem 4: f_r(m) >= 2(r-1) binom(m,2) + m Theorem 5: for r >= m >= 3, a lower bound on f_r(m) quadratic in r Theorem 6: f_r^k(m) >= m(r-1) floor((m-1)/(k-1)) + m Theorem 7: g_r^k(m) > rm floor((m-1)/(k-1))Theorem 8: f_r^k(m) <= g_r^k(m) <= (q^2-1)/t for a prime power q = 1 mod t, q >= r(m+1)-1, t < k Generalized Split Graphs and Ramsey Numbers Proposition 2 (p. 257): (p+2,q+2)-Ramsey graphs are (p,q)-split critical Problems close to my heart Conjecture 2.4 (p. 5): every r-coloring of K_{r^2+1} has r+1 vertices missing a color A finite basis characterization of α-split colorings Construction (p. 421): infinitely many critical colorings for the Erdős–Gyárfás three-color split partition

Graph