VibeMathedMath problems solved with AI
Sign in

The Erdős-Faudree-Rousseau-Schelp cycle-clique conjecture: R(Cm,Kn)=(m−1)(n−1)+1R(C_m,K_n)=(m-1)(n-1)+1 for m≥n≥3m\ge n\ge3

Erdős problem #551 · erdosproblems.com/551

Let R(Cm,Kn)R(C_m,K_n) be the least NN such that every red-blue colouring of the edges of KNK_N contains a red cycle of length exactly mm or a blue KnK_n. Taking n−1n-1 disjoint red cliques of order m−1m-1 with all edges between them blue gives R(Cm,Kn)≥(m−1)(n−1)+1R(C_m,K_n)\ge(m-1)(n-1)+1. Erdős, Faudree, Rousseau and Schelp (1978) conjectured equality for m≥n≥3m\ge n\ge3, apart from R(C3,K3)=6R(C_3,K_3)=6. Bondy and Erdős proved it for m≥n2−2m\ge n^2-2, Nikiforov for m≥4n+2m\ge4n+2, it was settled for n≤7n\le7, and Keevash, Long and Skokan (2021) proved it for m≥Clog⁡n/log⁡log⁡nm\ge C\log n/\log\log n with an unspecified absolute constant, leaving finitely many pairs that could not be listed. Is R(Cm,Kn)=(m−1)(n−1)+1R(C_m,K_n)=(m-1)(n-1)+1 for all m≥n≥3m\ge n\ge3 with (m,n)≠(3,3)(m,n)\ne(3,3)?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Graph Ramsey theory
Posed by
Paul Erdős, Ralph Faudree, Cecil Rousseau and Richard Schelp (J. Graph Theory 1978); Erdős Problem #551
Year posed
1978
Years open
48y
Solved
2026-09-25
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
21 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1: R(Cm,Kn)=(m−1)(n−1)+1R(C_m,K_n)=(m-1)(n-1)+1 for every m≥n≥3m\ge n\ge3 other than (3,3)(3,3), where R(C3,K3)=6R(C_3,K_3)=6. The proof takes a minimal counterexample (independent sets expand), finds a clique of order at least max⁡{3,⌊k/2⌋}\max\{3,\lfloor k/2\rfloor\}, optimizes path systems between clique vertices, and reduces the rest to 3,099 finite instances excluded by two exact programs. Keevash-Long-Skokan had already left only finitely many pairs open, without an explicit list; this result closes all of them. It does not address the side questions recorded with Problem #551 for fixed nn (the least cycle length at which the identity holds when m<nm<n is allowed, and the minimum of R(Ck,Kn)R(C_k,K_n) over kk).

What the AI did

The release README says all results in the release were produced by an unreleased internal OpenAI model with one fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This family is not among the README's exceptions (the Hodge conjecture for CM abelian varieties, and the Re(s) > 11/12 zero-free region whose write-up was human-edited). The manuscripts are authored 'OpenAI' and name no human author. The proof is computer-assisted: a structural reduction leaves 3,099 finite parameter-pattern instances, which accompanying programs exclude with deduction traces. The release also contains a Lean formalization of the full theorem.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1 and the history section were read against Erdős Problem #551 and the Keevash-Long-Skokan formulation. lean/docs/189.md links the challenge ComparatorChallenges/CycleCliqueRamsey (theorem OAI.CycleClique.thm_main, solution module OAI.Combinatorics.Ramsey.CycleClique.Main, whose file exists at the pinned commit); the challenge is not in the formalization catalogue formalization.yaml. The statement was read here: for all integers 3≤n≤m3\le n\le m with (m,n)≠(3,3)(m,n)\ne(3,3) the least NN such that every graph on NN vertices contains a copy of the mm-cycle or its complement contains KnK_n equals (m−1)(n−1)+1(m-1)(n-1)+1, and the value at (3,3)(3,3) is 6. That is the headline claim, including the finitely many computer-checked cases. Not rebuilt here.

Sources

Changelog1 change

Discussion