Erdős Problem #551

Read our full write-up →

Erdős, Faudree, Rousseau and Schelp conjectured in 1978 that R(C_m, K_n) = (m−1)(n−1)+1 for all m ≥ n; in its standard form, with n ≥ 3 and (3,3) excepted, it is Erdős problem #551. Keevash, Long and Skokan proved it in 2021 for m ≥ C log n / log log n. That settles every large n but leaves finitely many pairs, and since their C is not explicit, not even the list of open pairs was known; Terence Tao noted on the problem page in September 2025 that the problem was decidable but still open. OpenAI's 6 October release claims all of it. The proof takes a minimal counterexample, finds a clique of order at least max{3, ⌊(m−1)/2⌋}, rules out cliques of order 9 or more by hand, and reduces the rest to 3,099 finite patterns of paths between clique vertices; two Python programs and, by a different encoding, a Lean proof each exclude them all. We read §§2–9 line by line and found no gap; two hostile AI referee seats on the mathematics (the t ≥ 9 argument, and the finite stage with its code) and one on the sources agreed. Our own enumerator reproduces the 3,099 patterns, both checkers re-run clean, and the Lean proof of the comparator's theorem (182 modules) replays on our machine with the standard axioms and a matching statement. A kernel-checked bridge of ours carries OpenAI's theorem to a verbatim copy of Formal Conjectures' erdos_551, which is still marked open there, with a pull request to close it waiting on a checked formal proof. Nothing in the theorem is ours.