The cycle–clique Ramsey conjecture

The cycle–clique Ramsey conjecture of Erdős, Faudree, Rousseau and Schelp asks for the exact Ramsey number of a cycle against a complete graph: R(C_m, K_n) = (m − 1)(n − 1) + 1 whenever m ≥ n ≥ 3, except for m = n = 3. It is Problem 551 on the Erdős problems site. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the full conjecture, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • The lower bound comes from n − 1 disjoint red cliques of order m − 1 with all edges between them blue.
  • The case n = 3 goes back to Chartrand and Schuster, and Bondy and Erdős proved the formula when m ≥ n² − 2. The full range was established for n = 4, 5, 6 and 7 by Yang–Huang–Zhang, Bollobás and coauthors, Schiermeyer, and Chen–Cheng–Zhang, with further cases for n = 8. Nikiforov stated the formula for n ≥ 4 and m ≥ 4n + 2.
  • Keevash, Long and Skokan proved the formula whenever m is at least an absolute constant times log n divided by log log n. This covers all sufficiently large n and leaves at most finitely many pairs open.
• The Erdős problems page for Problem 551 (accessed 17 October 2026) records the same partial results and lists no proof claims. A comment by T. Tao of 1 September 2025 notes that the problem had been reduced to a decidable, finitary problem but was still open.

The original result

• Cycle–clique Ramsey numbers (25 September 2026). Theorem 1.1 of the manuscript states that R(C_m, K_n) = (m − 1)(n − 1) + 1 for all integers m ≥ n ≥ 3 other than m = n = 3, and that R(C₃, K₃) = 6. The manuscript states that this establishes the conjecture in the formulation of Keevash, Long and Skokan, and that its finite calculation does not need a numerical value of their constant.
  • Method, as described: a minimal counterexample has an expansion property for independent sets. It contains a clique of order at least the larger of 3 and half the cycle length, found by distance layers and path rotation. Maximal systems of paths through a maximum clique are then constrained by the absence of the target cycle. Large cliques are excluded by an independence count. The remaining cases, with clique order 3 to 8, form 3,099 parameter-pattern instances that are excluded by proved inference rules. The manuscript describes two separate exact implementations of this enumeration.
• Sources. Commit 1581d4c of the openai/math repository, folder Cycle–clique Ramsey numbers.
• Formalization, as described by the repository. The scope note lean/docs/189.md states that the formalization proves the formula for all m ≥ n ≥ 3 except the pair (3, 3), where it proves the value 6, which is the complete parameter range of the main theorem. The Comparator statement is CycleCliqueRamsey.
• Kernel records. In the con-leche development journal's run over all 416 Comparator challenges of the collection (repository commit fd4aeeb, run of 10 October 2026; DESIGN.md, task #348), con-leche and Lean's official kernel both accepted 401 challenges; CycleCliqueRamsey is not among the 15 named exceptions.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
2026-10-08	Formal Conjectures pull request #6992	Catalogue proposal	Proposes marking the Formal Conjectures statement of Erdős Problem 551 as solved, citing Theorem 1.1 of the OpenAI manuscript at commit adc7f12. It adds no formal proof link and notes that the external proof was not built locally.	Open. The statement on the main branch is still marked open.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.