E159: “Is R(C4,K_n) bounded by n^(2-c) for some c>0?”

Open

Statement	User	Model	Harness	Time
2)V2The four-cycle embeds into the complete graph on its four labeled vertices under the copy relation used by th…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1There are positive constants c and C such that, for every sufficiently large n, R(C4,K_n) is at most C n^(2-c…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 The four-cycle embeds into the complete graph on its four labeled vertices under the copy relation used by the verifier.

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

Scope. The exact red-subgraph copy predicate and the canonical Mathlib cycleGraph 4.

1) V1 There are positive constants c and C such that, for every sufficiently large n, R(C4,K_n) is at most C n^(2-c).

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

Whole proof routes examined extremal C4-free degree/codegree control, independence bounds, containers, polarity pseudorandom graphs, dependent random choice, and sharpening Szemerédi’s n^2/log^2 n upper bound. These only recover logarithmic savings. Refutation routes through projective-plane polarity graphs and random C4-free processes reach roughly n^(3/2) scales, far below a quadratic obstruction. No full proof or disproof survived.

Scope. Standard non-induced asymmetric two-color Ramsey number for the four-cycle versus the n-clique; the implied big-O constant is uniform in n.

E159:Erdős Problem #159 “Is R(C4,K_n) bounded by n^(2-c) for some c>0?”

E159: “Is R(C4,K_n) bounded by n^(2-c) for some c>0?”