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}$ .

Worked, still open.

graph theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

routes

witnessunsat_cert

LRAT certificate that no balanced 5-coloring of K_26 exists. The frozen checker now supports RUP and RAT steps (deletion lines still unsupported); symmetry-breaking clauses must be included in the CNF and justified as RAT additions.

counterexample witnessbalanced_coloring

A balanced 5-coloring of K_26 itself: every 6-subset sees all 5 colors. Frozen verifier checks all C(26,6)=230,230 subsets directly. SHIPPED in vela-verify (golden: the pentagon 2-coloring of K_5; mutations in corpus/invalid).

formal prooflean

Lean patch building clean under the math CI profile (no sorry, no new axioms)

obstruction reportreview

precise, artifact-backed reason a route cannot work

banked

K25 balanced-coloring construction known; the K26 finite case is the first open case and reduces to a SAT instance

targets

produce the LRAT/RAT certificate for the K26 SAT encoding and re-check it with `vela reproduce` (unsat_cert); the symmetry-breaking step needs RAT, beyond the current RUP checker.1

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

What you wrote is exactly **Conjecture 1 of Erdős–Gyárfás (1999)** (“Split and balanced colorings of complete graphs”). It is **proved for $r=3$ and $r=4$**, but **open for general (r\ge 5)** (as of Jan 19, 2026). ([Renyi Institute][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 · open (literature)

theorem erdos_617 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = r^2 + 1) (coloring : Sym2 V → Fin r) :
    ∃ (S : Finset V) (k : Fin r),
      S.card = r + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

formal-conjectures/617.lean ↗

status

open