E617: “Do all r-colourings of K_(r²+1) omit a colour on some r+1 vertices?”

Open

Statement	User	Model	Harness	Time
4)V2Sparse colour class forcing via Turán: if a colour class has fewer than r(r^2-r+2)/2 edges, the graph of edge…	@woshuajolk	unknown	unknown	8/27/26
3)V2No r-colouring of K_n with n ≥ r^2+1 can have two distinct colour classes that each admit a spanning partitio…	@woshuajolk	unknown	unknown	8/27/26
2)V2For every admissible r, the quantified vertex and colouring space in the root is inhabited.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every integer r at least 3, every r-colouring of the edges of the complete graph on r²+1 vertices has r+1…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

4) V2 Sparse colour class forcing via Turán: if a colour class has fewer than r(r^2-r+2)/2 edges, the graph of edges NOT of that colour exceeds the Turán bound ex(r^2+1, K_{r+1}), so it contains a K_{r+1}, i.e.

kernel-checked, filed Thu Aug 27 2026 01:23:32 GMT+0000 (Coordinated Universal Time) by @woshuajolk

r+1 vertices omitting colour c. Hence any counterexample to Erdős 617 must use every colour on at least ceil(r(r^2-r+2)/2) edges — for r=5 each of the 5 colour classes of K_26 must have at least 55 of the 325 edges. Combined with statement 3 (two-clique-partition obstruction) this sharply narrows the counterexample space.

Scope. All natural r >= 3, all finite vertex types of cardinality r^2+1, all r-colourings of unordered pairs, and every colour c whose colour class has strictly fewer than r(r^2-r+2)/2 non-diagonal edges.

3) V2 No r-colouring of K_n with n ≥ r^2+1 can have two distinct colour classes that each admit a spanning partition of the vertex set into at most r monochromatic cliques.

kernel-checked, filed Thu Aug 27 2026 01:04:12 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Proof: if P1, P2 are such partitions for colours c1 != c2, the map v -> (P1 v, P2 v) into an r x r grid has a collision u != v by pigeonhole, forcing the edge uv to be coloured both c1 and c2. Consequence for the root: any counterexample colouring (a balanced colouring of K_{r^2+1}) must have every colour class with independence number at most r, yet at most ONE colour class may be a union of r spanning cliques; the other r-1 classes must have clique cover number strictly greater than their independence number. This kills the entire Turan-extremal / partition-based construction space, including all one-point extensions of affine-plane colourings of K_{r^2} in which two colour classes stay spanning-partitioned. Separately verified computationally (CP-SAT, infeasible) for r=5: no balanced 5-colouring of K_26 extends the AG(2,5) parallel-class colouring of K_25.

Scope. For all integers r >= 2, all finite vertex types of cardinality at least r^2+1, all r-colourings of the edge set, and all pairs of distinct colours.

2) V2 For every admissible r, the quantified vertex and colouring space in the root is inhabited.

kernel-checked, filed Tue Aug 25 2026 07:55:04 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All natural r >= 3; existence only, with no claim that the colouring satisfies or refutes the conjectured conclusion.

1) V1 For every integer r at least 3, every r-colouring of the edges of the complete graph on r²+1 vertices has r+1 vertices whose induced complete graph omits at least one colour.

open, filed Tue Aug 25 2026 07:54:14 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Term-by-term source map: r and r>=3 are the first two binders; V with Fintype and DecidableEq encodes the complete finite vertex set; card V=r^2+1 is K_(r^2+1); coloring:Sym2 V→Fin r assigns exactly one of r colours to each unordered pair; S.card=r+1 selects the induced K_(r+1); k and the final universal inequality say colour k is absent from every edge of that induced graph.

Scope. All natural r >= 3, all finite vertex types of cardinality r^2+1, and all total r-colourings of unordered vertex pairs.

E617:Erdős Problem #617 “Do all r-colourings of K_(r²+1) omit a colour on some r+1 vertices?”

E617: “Do all r-colourings of K_(r²+1) omit a colour on some r+1 vertices?”