Claims

../

1978_01_01_chung_liu: Theorem 3.6 of Chung and Liu (Discrete Math. 1978) shows that every three-coloring of K_10 has four vertices missing a color, the case r = 3 of Problem 617, with a coloring of K_9 showing it sharp; refereed.

1999_04_01_erdos_gyarfas: Lemmas 1 and 2 of Erdős and Gyárfás (Discrete Math. 1999) show that every three-coloring of K_10 and every four-coloring of K_17 has r + 1 vertices missing a color, the cases r = 3 and r = 4 of Problem 617; refereed.

2026_07_18_sneiderman_r5: A preprint of 18 July 2026 claims the fixed case r = 5 of Problem 617: every five-coloring of K_26 has six vertices missing a color, while K_25 has one without; with Kara's Lean and LRAT formalization of the argument; claimed.

2026_07_18_sneiderman_r6: A preprint of 18 July 2026 claims the fixed case r = 6 of Problem 617: every six-coloring of K_37 has seven vertices missing a color, by clique lemmas on 18, 19, 24 and 25 vertices and an edge count on 31; unrefereed, so claimed.

2026_07_20_sneiderman_r7_r8: A preprint of 20 July 2026 claims the fixed cases r = 7 and r = 8 of Problem 617 (K_50 with seven colors, K_65 with eight), by a colored-density reduction closed by an exhaustive lemma and 862 LRAT-checked instances; claimed.

2026_07_21_silverstein: A write-up of 21 July 2026 claims the fixed case r = 5 of Problem 617 by a one-color count: each color class needs 66 edges, five need 330 of the 325 edges of K_26; twelve DRAT-certified formulas; unrefereed, so claimed.

2026_07_21_sneiderman_r9: A preprint of 21 July 2026 claims the fixed case r = 9 of Problem 617: every nine-coloring of K_82 has ten vertices missing a color, by a density recursion reduced to finite statements on 26 and 27 vertices; unrefereed, so claimed.

2026_07_25_rose: A paper of 25 July 2026 by Anthony Rose claims the fixed case r = 5 of Problem 617 by scaling the Erdős–Gyárfás minority-color technique down to 458 SAT instances, all refuted with DRAT proofs; unrefereed, so claimed.

2026_07_31_winter: A repository and write-up of 31 July 2026 by Nick Winter claim the fixed case r = 5 of Problem 617 with a Lean 4 proof, by a hitter lemma and a minority-color lemma; the SAT certificates rest on native_decide; claimed.

2026_08_11_terpstra: A preprint draft and artifact released on 11 August 2026 by Adam Lee Terpstra, written by OpenAI Codex under his direction, claim the fixed cases r = 10 and r = 11 of Problem 617 with no certificate; unrefereed, so claimed.

---