View source for 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''<sub>''m''</sub>, ''K''<sub>''n''</sub>) = (''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 ([https://github.com/openai/math 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''<sup>2</sup> − 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'' ≥ 4''n'' + 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 [https://www.erdosproblems.com/551 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''<sub>''m''</sub>, ''K''<sub>''n''</sub>) = (''m'' − 1)(''n'' − 1) + 1 for all integers ''m'' ≥ ''n'' ≥ 3 other than ''m'' = ''n'' = 3, and that R(''C''<sub>3</sub>, ''K''<sub>3</sub>) = 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 <code>1581d4c</code> of the openai/math repository, folder [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Cycle-clique-Ramsey-numbers-September-25-2026 Cycle–clique Ramsey numbers].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/189.md 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 <code>CycleCliqueRamsey</code>.
* '''Kernel records.''' In the con-leche development journal's run over all 416 Comparator challenges of the collection (repository commit <code>fd4aeeb</code>, run of 10 October 2026; [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md <code>DESIGN.md</code>], task #348), con-leche and Lean's official kernel both accepted 401 challenges; <code>CycleCliqueRamsey</code> is not among the 15 named exceptions.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 17 October 2026)
|-
| 2026-10-08 || Formal Conjectures [https://github.com/google-deepmind/formal-conjectures/pull/6992 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 <code>adc7f12</code>. 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.

[[Category:OpenAI results]]