AI Proved What?

Episode 189, October 2026

Red cycle or blue clique?

A preprint claims that exactly (m−1)(n−1)+1 dots force a red cycle through m dots or a blue clique of n dots, for every m ≥ n ≥ 3 except the triangle pair, where the answer is 6

Covers result 189 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 189: Red cycle or blue clique? Twelve dots in three groups of four, every link inside a group red and every link between groups blue: the classical colouring with no red 5-cycle and no blue 4-clique.

6:46. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 2:00The claim
  3. 3:15How the proof goes
  4. 5:47Where it stands

The claim, in plain words

Colour every link of a complete network red or blue. The Ramsey number R(Cm, Kn) is the number of dots that forces a red cycle through exactly m dots or n dots all joined in blue. Splitting (m−1)(n−1) dots into n−1 groups of m−1, red inside the groups and blue between, avoids both: a red cycle stays in one group, which is too small, and a blue clique takes at most one dot per group. Triangles are special: a red pentagon with its blue pentagram has no one-colour triangle, so R(C3, K3) = 6, not 5.

The paper credits the conjecture that one more dot always suffices to Erdős, Faudree, Rousseau and Schelp (1978), in the form stated by Keevash, Long and Skokan. As the paper lists it, the triangle case goes back to Chartrand and Schuster; Bondy and Erdős proved it for m ≥ n² − 2; all m were settled for cliques of 4, 5, 6 and 7 dots in papers from 1999 to 2008, and parts of the case of 8; Nikiforov’s paper states it for n ≥ 4 and m ≥ 4n + 2; and Keevash, Long and Skokan proved it whenever m is at least a constant times log n / log log n, which, as the paper puts it, leaves at most finitely many pairs. Which pairs depends on their constant, which they do not give; the new proof never needs it.

Result 189 is one OpenAI preprint, Cycle–clique Ramsey numbers (41 pages, dated September 25, 2026). Its Theorem 1.1: for all integers m ≥ n ≥ 3 with (m, n) ≠ (3, 3), R(Cm, Kn) = (m−1)(n−1)+1, and R(C3, K3) = 6. The lower bound is the classical construction; the new content is the upper bound for every pair in the range. The last step is computer-assisted: the paper reduces the remaining cases to 3,099 finite patterns and refutes every one with two separate programs, which accompany the paper.

What it doesn’t claim

Anything for cycles shorter than the clique size (m < n). A new lower-bound construction, or a classification of the colourings that come closest (our search finds more than one). The proof does not use Keevash, Long and Skokan’s theorem or its constant. And the computer does not search through graphs or colourings: it checks patterns of paths, using inference rules proved in the paper.

Where it stands

Posted as a preprint
OpenAI, 41 pages, dated September 25, 2026, with programs and deduction traces
Peer reviewed
Not yet
Checked in Lean
The theorem, exactly as stated with the triangle exception, formalized by OpenAI; not run by us

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. We ran the paper’s compact checker on a copy: its output matches the paper’s Table 2 exactly. OpenAI published a Lean formalization: the comparator statement is Theorem 1.1 with the triangle exception, and every finite case is re-checked by Lean’s kernel rather than by the Python programs. By our count the main proof route takes 182 files and about 78,000 lines, excluding Mathlib (source); the full module adds a second, independent development, for 443 files and about 2.8 million lines, almost all of it machine-generated certificate data. We found no unproved steps by search; we have not rebuilt the proof. The collection’s formalization.yaml does not list this result. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. Red graph. Keep only the red links: a blue clique of n dots is an independent set of n dots. So the claim is that every graph on (m−1)(n−1)+1 dots has a cycle through exactly m dots or n independent dots.
  2. A smallest counterexample. Keep m fixed and take a counterexample with n as small as possible. Then any independent dots, together with their neighbours, cover a lot of the graph, or deleting them and their neighbours would leave a smaller counterexample (Lemma 2.2); every dot has at least m−1 neighbours. The paper credits this kind of expansion, and rooted distance layers, to Erdős, Faudree, Rousseau and Schelp.
  3. A large clique. Such a graph with no cycle of exactly m dots contains a clique of at least about half of m−1 dots (Theorem 3.1), via a crowded distance layer and Pósa-style path rotation. Cycles of 4 and 5 dots are done by hand.
  4. Paths through the clique. Paths hung between clique dots, with enough outside dots but not too many, close into a cycle of exactly m dots (Lemma 6.1). The best system below that line forces separated regions, each holding 2 or 3 independent dots; if the clique has 9 or more dots, that is too many (Proposition 8.4).
  5. The finite remainder. A clique of 3 to 8 dots and cycles of 6 to 18: a path system is described by a pattern (the number of inside dots on each path, chain by chain), 3,099 patterns over 42 parameter pairs. The programs apply the proved rules (forbidden outside paths, required paths, trial additions, packing): 3,049 refuted by the first packing test, 50 after further deductions, none left unresolved. Pósa rotation, a special case of Chvátal–Erdős, and a shortening argument of Radziszowski and Jin are re-proved in the paper.

The numbers in the video

  • Exhaustive search (ours; these values were known before): R(C3, K3) = 6; R(C4, K3) = 7, R(C5, K3) = 9, R(C6, K3) = 11, R(C4, K4) = 10, R(C5, K4) = 13, R(C6, K4) = 16. For m = 4, n = 3 the 6-dot colourings avoiding both come in two kinds: two red triangles, and two red triangles joined by one red link.
  • The lower-bound colouring checked for 3 ≤ n ≤ m ≤ 7, and the pentagon (ours).
  • Our own recount of the paper’s Table 1: 42 parameter pairs, 3,099 patterns, row by row; the bar chart shows patterns per cycle length from Table 1.
  • The map of which pairs the listed results cover is ours; the paper does not draw it.
  • The Lean count: our count of the import closures.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

Colour every link of a complete network red or blue. How many dots does it take to force one of two things: a red cycle through exactly m dots, or n dots all joined to each other in blue? That number is the Ramsey number of the m-cycle against the n-clique. Here is why it must be more than (m−1)(n−1). Split that many dots into n−1 groups of m−1 dots, colour every link inside a group red, and every link between groups blue. A red cycle stays inside one group, which is too small, and a blue clique can take only one dot from each group. With m = 4 and n = 3, that is two red triangles on 6 dots. Our exhaustive search confirms that 7 dots force a red 4-cycle or a blue triangle, and that the six-dot colourings that avoid both are not unique. The triangle is special: a red pentagon with its blue pentagram has neither colour’s triangle, so the answer there is 6, not 5. The paper credits the conjecture to Erdős, Faudree, Rousseau and Schelp, published in 1978, in the form stated by Keevash, Long and Skokan: for every m ≥ n ≥ 3, except (3,3), one more dot than that construction is always enough. Many cases were known. For triangles it goes back to Chartrand and Schuster; Bondy and Erdős proved it when the cycle is long, m ≥ n² − 2; the full ranges of m for cliques of 4, 5, 6 and 7 dots came in papers from 1999 to 2008, and parts of the case of 8. Nikiforov’s paper states it when m ≥ 4n + 2. And Keevash, Long and Skokan proved it whenever m is at least a constant times log n / log log n. As the paper puts it, that leaves at most finitely many pairs in the range. Which pairs depends on their constant, which they do not give, and the new proof never needs it.

2:00The claim

Result 189 is one OpenAI preprint, 41 pages, dated September 25, 2026. It claims: for all whole numbers m ≥ n ≥ 3, other than the pair (3,3), the Ramsey number of the m-cycle against the n-clique is (m−1)(n−1)+1; and for the triangle pair it is 6. The lower bound is the classical construction; the new content is the upper bound, for every pair in the range. The last step is computer-assisted: the paper reduces the remaining cases to 3,099 finite patterns, and refutes every one with two separate programs. We ran the compact one: its output matches the paper’s table exactly, and our own count of the patterns agrees. Not claimed: anything for cycles shorter than the clique size. No new lower-bound construction, and no classification of the colourings that come closest; our search already finds more than one. The proof does not use Keevash, Long and Skokan’s theorem or its constant. And the computer does not search through graphs or colourings: it checks patterns of paths, using rules proved in the paper. Our small exact values were known before; they only illustrate the formula.

3:15How the proof goes

Look only at the red links. A blue clique of n dots is then a set of n dots with no red link between them, an independent set. So the claim is: every graph on that many dots has a cycle through exactly m dots, or an independent set of n dots. Suppose not: keep m fixed, and take a counterexample with n as small as possible. Minimality forces expansion: any few independent dots, together with their neighbours, must cover a lot of the graph, because otherwise deleting them and their neighbours would leave a smaller counterexample. In particular, every dot has at least m−1 neighbours. The paper credits this kind of expansion, and rooted distance layers, to Erdős, Faudree, Rousseau and Schelp’s original argument. Next, an expanding graph with no cycle of exactly m dots must contain a large clique, of at least about half of m−1 dots. Grow a breadth-first tree from one dot; some distance layer is crowded; inside it, a path-rotation argument going back to Pósa finds a path of just the right length whose ends lie in different branches, and closing it through the tree would give a cycle of exactly the forbidden length, unless the clique is there. Cycles of 4 and 5 dots are finished by hand. Then the paper hangs paths between the clique’s dots. Because a clique lets you jump between any two of its dots, a system of such paths with enough outside dots, but not too many, closes into a cycle of exactly m dots. So take the best system that stays below that line: every improvement is forbidden, which forces separated regions, each holding 2 or 3 independent dots. If the clique has 9 or more dots, that is too many independent dots: a contradiction. What remains is a finite range: a clique of 3 to 8 dots, and cycles of 6 to 18. A path system is then described by a pattern, the number of inside dots on each path, chain by chain, and there are exactly 3,099 of them over 42 parameter pairs. For each pattern, the programs apply the proved rules, forbidden outside paths, required paths, trial additions, and packing, until they find more independent dots than allowed. Every pattern is refuted: 3,049 by the first packing test, 50 after further deductions, none left unresolved. Classical ingredients, Pósa rotation, a special case of Chvátal and Erdős, and a shortening argument from Radziszowski and Jin, are re-proved in the paper.

5:47Where it stands

The preprint is unrefereed and has not been revised. OpenAI’s Lean files state the theorem exactly, including the triangle exception, and prove it, with every finite case re-checked by Lean’s own kernel rather than by the Python programs; the main proof route is about 78,000 lines, with no gaps we could find by search. A second, independent Lean development sits in the same folder, which brings it to about 2.8 million lines, almost all of it machine-generated certificate data. We did not run the check. The paper is not among those OSVerify reviewed, and we have seen no expert review. If it holds, (m−1)(n−1)+1, dots are exactly what it takes to force a red cycle of m or a blue clique of n, for every m ≥ n ≥ 3, except the triangle pair, where the answer is 6.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.