#551: R(C_m, K_n) = (m−1)(n−1)+1 for every m ≥ n ≥ 3 except (3,3) — the Erdős–Faudree–Rousseau–Schelp cycle–clique conjecture, by OpenAI's 41-page proof: read line by line here, its 3,099-pattern finite stage recounted, re-run and re-validated, its Lean proof kernel-replayed on our machine, and carried by a kernel-checked bridge to Formal Conjectures' statement, which is still marked open

The problem (erdosproblems.com/551; [EFRS78]). "Prove that R(C_k, K_n) = (k−1)(n−1)+1 for k ≥ n ≥ 3 (except when n = k = 3)." Below we write m for the cycle length, as OpenAI does, and keep k for m − 1. The page records Bondy–Erdős 1973 for cycle length above n² − 2 (their Theorem 4 actually includes n² − 2 itself), Nikiforov 2005 for cycle length at least 4n + 2, and Keevash–Long–Skokan 2021 for cycle length at least C log n / log log n, "thus establishing the conjecture for sufficiently large n". Its one comment is Terence Tao's, 1 September 2025: "Technically the problem has been reduced to a decidable (finitary) problem, but is still open." There are no proof claims. The lower bound is the familiar one: n − 1 disjoint red cliques of order m − 1, all edges between them blue, contain no red C_m and no blue K_n. The whole question is the matching upper bound. The cases n ≤ 7 had each needed its own paper (n = 7 by Chen, Cheng and Zhang in 2008). For n = 8 only 8 ≤ m ≤ 15 had been settled directly, plus m ≥ 34 through Nikiforov's theorem, whose printed proof has a problem noted below; without it, Schiermeyer's range gives m ≥ 48 and Bondy–Erdős's m ≥ 62.

The claim. Cycle–clique Ramsey numbers (OpenAI, 41 pp., dated 25 September 2026) is family 189 in the openai/math release. Its directory first appeared in the repository's initial commit (adc7f12, 6 October 2026, 21:58:50 UTC) and is unchanged at today's head, 1581d4c. Theorem 1.1: for all m ≥ n ≥ 3 with (m, n) ≠ (3, 3), R(C_m, K_n) = (m−1)(n−1)+1, and R(C₃, K₃) = 6. The release carries a Lean proof of exactly this statement, two Python checkers for the finite stage, and a file of deduction traces. Thomas Bloom listed it on 8 October among the release's claims, with his standing caution that he had not checked any of them.

The argument. Write k = m − 1 and a = n − 1, so the range is k ≥ 3, 2 ≤ a ≤ k. Fix k and suppose the bound fails; choose the least failing a and a graph G on ka + 1 vertices with no cycle of exactly k + 1 vertices and no independent set of size a + 1. Minimality gives an expansion property: every nonempty independent set I has a closed neighbourhood of at least k|I| + 1 vertices, because deleting it leaves a smaller instance (§2). The proof then runs in four stages.

• A large clique (§3). G has a clique of order t ≥ max{3, ⌊k/2⌋}. A triangle comes from R(K₃, K_a+1) ≤ ka + 1, which settles k ≤ 7. For k ≥ 8, suppose there is no clique of order s = ⌊k/2⌋. A counting argument on the layers of a breadth-first tree finds one layer containing a connected, nonbipartite subgraph H with minimum degree at least s and an expansion property of its own. Let c be the lowest common ancestor in the tree of all vertices of H, p levels above them. If p = 1, a path on k vertices of H closes through c. Otherwise a Pósa-rotation argument gives a path inside H of length exactly k + 1 − 2p whose two ends lie under different branches at c, and with the tree path of length 2p between those ends it closes a cycle of exactly k + 1 vertices.
• k = 3 and 4 (§4) are done by hand. Around a triangle or a K₄, every short connection between the outside neighbourhoods of different clique vertices would close a C₄ or C₅, so those neighbourhoods are separated; expansion then makes them too big, and a short case analysis finishes.
• Cliques of order t ≥ 9 (§§5–8). Fix a maximum clique Q. A path system is a set of paths between vertices of Q with disjoint nonempty interiors outside Q, whose endpoint pairs form disjoint chains on Q (a linear forest). Choose one with the largest total interior below k + 1 − t, with the fewest paths on ties. Any system whose total lands in a certain interval closes into a C_k+1 through edges of Q, so optimality forbids a long list of improvements. Each clique vertex gets a representative: itself if it starts its chain, otherwise the first interior vertex of the path coming into it. If no two representatives were joined by a short path outside the system (at most six interior vertices), their radius-two neighbourhoods would be separated and hold more than k independent vertices (Lemma 7.4). So such a path exists, and it would be one of the forbidden improvements unless the system has one of exactly three shapes (Lemma 8.2). In each shape, balls around suitably chosen representatives are again pairwise separated and carry more than k independent vertices (Proposition 8.4), contradicting α(G) ≤ k. A lemma in §5 (after Chvátal–Erdős) turns "more than max{k, 2t} vertices" into "three independent vertices".
• t ≤ 8 (§9). Then k ≤ 2t + 1 ≤ 17. The optimal path system is recorded as a pattern: the sequence of interior-vertex counts along each chain, up to reversal and reordering, with total interior at most the budget k − t. The admissible pairs are 5 ≤ k ≤ 17 with max{3, ⌊k/2⌋} ≤ t ≤ min{8, k}: 42 of them, carrying 3,099 patterns. For each pattern the paper derives forbidden outside paths from optimality and from cycle closure, then grows balls and packs independent sets, adding a trial edge or one trial vertex where that is not enough. Every pattern ends in a contradiction: 3,049 at the first packing test and 50 after the required-path rule or strengthening.

The Lean, and our replay. The release has two Lean routes to the theorem, side by side in OAI/Combinatorics/Ramsey/CycleClique/. Route A is the one the comparator challenge ComparatorChallenges/CycleCliqueRamsey.lean names: OAI.CycleClique.thm_main, proved in MainTheorem.lean. Its import closure is 182 modules (28.3 MB of source, with about 43,000 decide proofs), and it follows the paper's case split exactly: reduced_counterexample_impossible sends k ≤ 4 to the small cases, clique number ≥ 9 to the t ≥ 9 argument, and everything else, after the clique bound, to the 42-pair finite verification. Route B is the 259 modules of Construction/ plus Main.lean and RamseyNumbers.lean: 261 modules and 194 MB outside route A's closure, with per-k certificates. It states the theorem as cycle_clique_main_unconditional (through an IsRamseyNumber predicate) and cycleCliqueRamsey_unconditional; we did not replay it. The release's own catalogue of formalized papers, lean/formalization.yaml, does not list this paper, although the scope note lean/docs/189.md and the comparator have been in the repository since the initial commit and the catalogue was revised the next day. Our source audit of all 443 modules found no axiom, sorry, native_decide, set_option, macro, elab, unsafe, implemented_by, extern, opaque or #eval. Our replay built all 182 modules of route A with 0 errors in 1 h 51 min of wall time (21:06 to 22:57 UTC on 20 October), with at most three lean processes at once; the largest peak in any one process was 7.8 GiB. #print axioms gives exactly propext, Classical.choice and Quot.sound for thm_main, and for main (the range m ≥ n ≥ 3, (m, n) ≠ (3, 3)), exceptional (R(C₃, K₃) = 6), ramsey_upper, the 42-pair finite_range_verified and the lower-bound construction. The theorem's type and both definitions it unfolds through, RamseyProperty and cycleCliqueRamsey, print identically under pp.all in the comparator challenge and in the solution. We mutation-tested the matcher on edited copies of those printouts: one character changed inside RamseyProperty's body (Fin → Fim), sorryAx deleted from the challenge's axiom list, and Lean.ofReduceBool added to the solution's. It flagged each one. A planted sorry is reported as sorryAx. Aiming thm_main at R(C₄, K₄) = 9 is rejected, because the term has type R(C₄, K₄) = (4−1)(4−1)+1; the same term aimed at that value elaborates. Mathlib's compiled files came from its cache, so we then ran leanchecker --fresh over the whole closure of MainTheorem, Mathlib included, which re-checks every declaration from scratch: exit code 0 after 11,486 s (a missing-module control exits 1). An independent replay came first: MathVet's fidelity review of the release logged a passing build and a passing run of OpenAI's comparator tool for this family on 19 October (axioms propext, Classical.choice, Quot.sound). Ours is a second, separate replay, with our own pp.all statement match in place of the comparator tool, plus the from-scratch check still running and the bridge below.

The finite stage: recounted, re-run and re-validated. We wrote our own enumerator of patterns, by brute force over multisets of chain types and sharing no code with the release. It reproduces every row of the paper's Table 1: 42 pairs, 3,099 patterns. Raising every budget by one gives 5,735 instead, so an off-by-one in the budget would have shown. The Lean files hard-code the pattern list for each pair; parsed out, all 42 lists equal our enumeration as sets, in canonical form, with no duplicates. Lowering every budget by one breaks 38 of the 42 pairs; the other four, with t = k, have budget 0 either way. The Lean also proves each list complete with a kernel-evaluated decide. We re-ran both released Python checkers unmodified. Each prints the published Table 2 rows byte for byte, and verify.py ends "Verified 3099 patterns in all 42 parameter pairs; zero unresolved" (51 s and 146 s; 197 s in all). Our finite-stage seat re-derived every inference rule of §9 from what §§2, 5 and 6 actually prove, and found none stronger than proved; §9 uses nothing from §§7–8. It also wrote a third validator from the paper's text. It rebuilds each pattern's initial matrix of forbidden outside paths by explicit path construction, and re-checks every deduction round and every final packing recorded in the shipped traces: 3,099 of 3,099 pass, and five negative controls fire. Mutation tests show nearly every rule doing work. For instance, the exceptional clause (9.11) of the ball bounds is needed exactly for the four patterns with t = k and no paths. One caution for anyone re-running the release. Deleting the degree test from Lemma 9.4 (the condition that both new endpoints have degree at most one in the old forest) makes that rule unsound. In the original checker it changes 2,471 of the 3,099 initial matrices, yet leaves the printed results table byte-identical, so a matching table proves little. What catches it is a check of the matrices themselves: the seat confirmed that the original checker's initial matrices equal those in the shipped trace for all 3,099 patterns, and that both equal its explicit-construction derivation. verify.py compares only the independent checker's regenerated trace with the shipped file; that would catch such a change in the independent program, not in the original.

The reading. The main seat (Claude, this entry's author) read §§2–9 line by line, re-deriving the inequalities, vertex counts and case splits, and found nothing above exposition; what it re-derived is recorded in the bundle as seats/main_reading.md. §§2–4 had that one reader. Three hostile AI referee seats then worked separately: a proof seat on §§5–8, a finite-stage seat on §9 and Appendix A, and a sources seat, seat W, on §1 and the literature. The proof seat found §§5–8 HOLDS AS READ. It also brute-forced the arithmetic of §8 for every t up to 70. And it model-checked, at the level of path systems (forest plus amounts), the replacement arguments of Lemmas 7.1, 8.1 and 8.2, the two-chain claim of Lemma 8.3, and, for every final packing, that each required pair of bases has its whole range of short paths forbidden and that the paper's per-ball independence values sum to more than k. That is about 79 million replacement systems for t = 9 to 12 and every k from t to 2t + 1, with no violation. The same program at t = 8, where Lemma 8.1 is not claimed, reports 169 violations, so the check can fail. The graph-level steps it took from the paper (ball growth, ball sizes, the per-ball triples) it checked by hand. It brute-forced the size test (Lemma 5.3) over every graph with no independent triple on up to 11 vertices. Its notes are wording only; for example, Lemma 8.2's proof takes d ≥ 2 from inside the proof of Lemma 8.1, and the letters a, v and r carry several meanings in §§7–8. The finite-stage seat also found HOLDS AS READ. It made two notes: the set E in Lemma 9.4 must be read as any admissible subset, not one fixed set; and verify.py should check the matrices against an explicit construction, not only the printed table. So the shape the paper claims is the shape it has: k = 3 and 4 by hand, cliques of order 9 or more by hand, and only t ≤ 8 by computer.

Formal Conjectures, and the bridge (ours). Formal Conjectures' Erdos551.erdos_551 (in FormalConjectures/ErdosProblems/551.lean) states the conjecture with its own SimpleGraph.graphRamsey: the least N such that every graph on Fin N contains the first graph or has the second in its complement. Its k is the cycle length. It is tagged research open and links no proof. A pull request to mark it solved (#6992, 8 October) has one approving review. A maintainer asked for a pinned formal proof, and the author replied that the link was pending because they had not yet checked the proof's axiom closure. We copied its graphRamsey and both of its statements (repository head 90d18f66, 20 October) into OpenAI's environment. The definitions and statements are character-identical; they are wrapped in an outer namespace Bridge551, with the attributes and docstrings dropped. We proved them from OAI.CycleClique.main. The two Ramsey numbers are the same infimum once completeGraph is unfolded to ⊤, so the main statement is a rewrite and rfl, and the sufficiently_large variant follows with threshold 4. Both depend only on propext, Classical.choice and Quot.sound. Two controls fail at the step meant to catch them: a wrong value, (k−1)(n−1) without the +1, fails at the rewrite, and a shifted cycle length (cycleGraph (k+1) in place of cycleGraph k) fails at rfl. Formal Conjectures' module cannot be imported into OpenAI's environment, because the toolchains differ, so this checks a verbatim copy of its statement, not its constant. We have staged a comment for that pull request with these results, and posted nothing.

Sources and the world. Every prior-result sentence in §1.1 agrees with its source. We read the primary text for all but five (Chartrand–Schuster, Schiermeyer, Zhang–Zhang, Bataineh–Jaradat–Al-Zaleq, and the journal version of Nikiforov), which we checked through abstracts, titles and later citations. Bondy–Erdős's Theorem 4 includes n² − 2 on the rendered page, which the problem page's "k > n² − 2" leaves out. The paper omits Schiermeyer's 2003 range m ≥ n(n − 2), which Nikiforov's supersedes for n ≥ 7. It also omits Faudree and Schelp's 1976 Kalamazoo paper (LNM 642, 1978), which the survey literature credits with first asking the same question; we have not seen its text. It is right to cite the conjecture "in the formulation stated by Keevash, Long and Skokan": the 1978 paper's own sentence, "It is conjectured that this formula holds for all m ≥ n", has no (3,3) exception. We found no other claim of the full conjecture and no public referee of the mathematics. Thomas Bloom's 8 October post lists it among claims he had not checked. The same 1978 page asks two more questions, and the problem page repeats them, the second as "the minimum value of R(C_k, K_n)": the smallest m at which the formula starts to hold, and which m minimises R(C_m, K_n) for fixed n. Keevash, Long and Skokan answered both up to a constant (m = Θ(log n / log log n)). This paper addresses neither, and known small values show the formula already holding below m = n (R(C₅, K₈) = 29 = 4·7 + 1). Two notes in passing. Our July report on this problem said that the printed proof of Nikiforov's range m ≥ 4n + 2 has a step in Case 4.1 that does not follow as written. Seat W re-checked it against the rendered pages of arXiv v1, the only arXiv version; we have not seen the journal text. Nikiforov proves r(K_r+1, C_p+1) = pr + 1 for p ≥ 4r + 5, so r = n − 1 and p = m − 1, and in Case 4.1 r₁ and r₂ are the independence numbers of an end block of the graph and of the rest. His displayed chain needs 2(r₁ + r₂) ≤ r + 1, where only r₁ + r₂ ≤ r + 1 and r₁ ≤ (r + 1)/2 are established; r = 6, p = 29, r₁ = 2, r₂ = 5 makes its second inequality read 37 ≤ 30. We found no erratum. Nothing here depends on it: OpenAI's proof never uses Nikiforov, its introduction says only that his Theorem 1 "states" the formula, and its own Theorem 1.1 covers that range. And the current Small Ramsey Numbers survey (DS1.18, April 2026, Table Vb) prints R(C₈, K₉) = 56, below the trivial lower bound of 57: eight disjoint copies of K₇ have 56 vertices, no C₈ and no independent set of size 9. Presumably 57 is meant.

What this entry is. The theorem, its paper proof and both of its Lean routes are OpenAI's. The problem was open until their release. The warrant for calling it closed is route A's Lean proof, kernel-checked on our machine with its statement matched to the conjecture; no human has refereed the paper's prose, as far as we can find. Ours: the replay and its controls; the recount of the patterns and the comparison with the Lean's lists; the re-run of the two checkers; the bridge to Formal Conjectures' statement; and the readings. In our labels ((a) proved in the text by elementary means, (d) computer-assisted): the structural argument of §§2–8 is (a), read line by line by the main seat, with §§5–8 read again by a separate proof seat; the finite stage is (d). Its patterns are excluded by two released Python programs, which share the labelling and the ball-bound arithmetic; by a Lean proof that re-checks explicit witness certificates in the kernel; and, for the recorded deductions, by our seat's validator of the shipped traces. The inference rules themselves were re-derived by hand, since an unsound rule would be copied into both programs. Every referee seat, and the main session, was served by Claude Opus 5.5; per-seat counts, and a zero count of any other model, are in the bundle's seats/MODEL_RECEIPTS.txt.