Cycle–clique Ramsey numbers

1 paperLean

Proves the Erdős–Faudree–Rousseau–Schelp conjecture: \(R(C_m,K_n)=(m-1)(n-1)+1\) for every \(m\ge n\ge3\), except \(R(C_3,K_3)=6\). This is the exact threshold forcing a red m-cycle or a blue n-clique in every red–blue coloring of a complete graph.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Cycle--clique Ramsey numbers

OpenAI · September 25, 2026

We prove that \(R(C_m,K_n)=(m-1)(n-1)+1\) for every pair of integers \(m\ge n\ge3\) other than \((m,n)=(3,3)\), for which \(R(C_3,K_3)=6\). This establishes the cycle–clique conjecture of Erdős, Faudree, Rousseau and Schelp. The proof combines expansion in a minimal counterexample with a large-clique lemma and an optimization of paths joining clique vertices. These arguments reduce the remaining cases to \(3{,}099\) finite parameter-pattern instances, which are excluded by two exact implementations of proved inference rules. Complete programs and deduction traces accompany the paper.

Read PDF Download Source

Cite

@misc{OAI:Cycle-clique-Ramsey-numbers-September-25-2026,
  author = {{OpenAI}},
  title = {{Cycle--clique Ramsey numbers}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Cycle-clique-Ramsey-numbers-September-25-2026/Cycle-clique-Ramsey-numbers-September-25-2026.pdf}{OAI:Cycle-clique-Ramsey-numbers-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Cycle–clique Ramsey numbers

Scope

The cycle–clique Ramsey conjecture predicts the exact number of vertices forcing either a cycle \(C_m\) or a clique \(K_n\) in complementary colors. The formalization proves \(R(C_m,K_n)=(m-1)(n-1)+1\) for all integers \(m\ge n\ge3\) except \((m,n)=(3,3)\), where it proves \(R(C_3,K_3)=6\). This is the complete parameter range of the paper's main theorem.

Comparator links

Result	Comparator statement
Exact cycle–clique Ramsey numbers	CycleCliqueRamsey.lean

Scope note on GitHub →