---

Claim. The preprint Cycle--clique Ramsey numbers of the OpenAI mathematics release (dated 25 September 2026, authored by OpenAI; the release's README states that its manuscripts were produced by an internal OpenAI model, which it does not name, so the claimant is the organization, and that the collection includes results at different stages of verification, not all with accompanying Lean formalizations), carded at openai_2026_cycle_clique_ramsey_numbers with the result pages Theorem 1.1 and Proposition 9.1, states as its Theorem 1.1 that for all integers $m\ge n\ge3$ with $(m,n)\ne(3,3)$

$$R(C_m,K_n)=(m-1)(n-1)+1,$$

and $R(C_3,K_3)=6$ for the excluded pair. In the letters of Problem 551 this is the displayed identity for every $k\ge n\ge3$ except $n=k=3$: the whole conjecture of Erdős, Faudree, Rousseau and Schelp in the formulation of Keevash, Long and Skokan, which the manuscript names as what it establishes. Its introduction records the prior ranges on the problem page (Bondy and Erdős for $k\ge n^2-2$, Nikiforov for $k\ge4n+2$, Keevash, Long and Skokan for $k\ge C\log n/\log\log n$) and the small cases $n\le7$ and parts of $n=8$ from the literature, and says that its finite calculation comes from an explicit structural reduction and needs no numerical value of the Keevash--Long--Skokan constant.

Method and read depth. By the introduction and the closing section, the proof takes a minimal counterexample, a graph with no cycle of order $k+1$ ($k=m-1$) and independence number at most $k$, and shows that every nonempty independent set has at least $k|I|+1$ vertices in its closed neighborhood; it finds a clique of order at least $\max\{3,\lfloor k/2\rfloor\}$ through distance layers and path rotations, settles $k=3,4$ directly, and for $k\ge5$ fixes a maximum clique and optimizes a system of paths between its vertices, whose forbidden improvements make neighborhoods disjoint and supply too many independent vertices when the clique has order at least 9. The remaining cases, clique order $3\le t\le8$ and $5\le k\le17$, are reduced to $3{,}099$ parameter-pattern instances over $42$ pairs $(k,t)$, each excluded by proved inference rules (path replacement, exact-cycle closure, neighborhood growth, independent-set packing, and contradiction under an added edge or path); two exact Python programs using only the standard library, a compact one reproduced in the appendix and an independently written one, enumerate the patterns and report the same table (no instance unresolved), and a wrapper runs both and compares their output and the generated deduction traces with the supplied files. Read depth: the abstract, introduction, finite-results section and implementation appendix are checked against the release's TeX source with the verification folder's file list and wrapper; the structural proof is not checked, and this corpus has not run the checkers.

Depends on. Nothing in this wiki; the manuscript says all structural arguments and inference rules are proved in its text, and it does not rely on the Keevash--Long--Skokan constant. The accepted partial claim Keevash, Long and Skokan 2021 is the context this result completes, not an input to it.

Formalization. The release's Lean tree at the pinned revision (its lean/ folder, the formalization link above) states the theorem in ComparatorChallenges/CycleCliqueRamsey.lean (OAI.CycleClique.thm_main: for all integers $m,n$ with $3\le n\le m$ and $(m,n)\ne(3,3)$, cycleCliqueRamsey of their natural parts equals $(m-1)(n-1)+1$, and cycleCliqueRamsey 3 3 = 6, where cycleCliqueRamsey m n is the least $N$ such that every simple graph on $N$ vertices contains $C_m$ or its complement contains $K_n$), with sorry as the challenge form, and holds a solution module OAI/Combinatorics/Ramsey/CycleClique/ whose MainTheorem.lean proves thm_main and whose Main.lean, imported by the project's root module, also proves cycleCliqueRamsey_unconditional for every $3\le n\le m$; the module carries pattern files for the $42$ pairs and ninety-seven certificate files. The comparator record permits only propext, Quot.sound and Classical.choice. The release's scope statement for this family, lean/docs/189.md, says the formalization proves the identity for all integers $m\ge n\ge3$ except $(3,3)$, where it proves $R(C_3,K_3)=6$, the complete parameter range of the paper's main theorem, and links the comparator statement; the release's catalog formalization.yaml alone lacks an entry for it. Toolchain leanprover/lean4:v4.34.1. The build of thm_main and the comparison of its statement with the problem's are recorded under Acceptance.

Acceptance. Formalized. This corpus's verification built OAI.CycleClique.thm_main at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked its axioms, which are exactly propext, Classical.choice and Quot.sound, with no sorry; the comparator challenge ComparatorChallenges/CycleCliqueRamsey.lean pins the declaration, and its fingerprint was found identical to the challenge. The statement agrees with the problem's: SimpleGraph.cycleGraph m is the cycle $C_m$ for $m\ge3$; the containment ⊑ asks for a copy that need not be induced, the right notion for the cycle; (⊤ : SimpleGraph (Fin n)) ⊑ Gᶜ says that $G$ has $n$ pairwise nonadjacent vertices; and cycleCliqueRamsey m n, the infimum of the $N$ with that property, is equated to positive values, so the set is nonempty and the value is its least element, the Ramsey number, never the junk value $0$ of an empty infimum. Under $3\le n\le m$ the natural parts of the integers are exact, the right side is computed in the integers without truncated subtraction, and $(m,n)\ne(3,3)$ is exactly the site's exception $n=k=3$. The first conjunct is the problem's Statement for every $k\ge n\ge3$ except $n=k=3$, and the second is the value $R(C_3,K_3)=6$ the manuscript also states, so the claim is full. Not reviewed: the manuscript is a release preprint with no journal record and no outside review known here, and the release's README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification; its structural proof and its two checkers are not checked or run here, and the Lean proof is the evidence. The site's page for Problem 551 showed DECIDABLE with an empty proof-claim tab on 2026-09-17. The result closes the finite residue left by the refereed theorems and settles the problem.