Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 551
claims/: The 4 claim pages of Problem 551, one per claimant's result; the problem's standing derives from them.
Statement. Prove that
for (except when ).
Formulation. The site's wording(the page shows no last-edited date). is the least such that every -coloring of the edges of has a red cycle of length or a blue ; equivalently, the least such that every -free graph on vertices has independent vertices, which is the form the sources use. The sources write the cycle length first but with other letters: in [BoEr73] (there is the cycle length), in [EFRS78], in [Ni05] and in [KLS21]; this page uses the site's and . The inequality holds for every and by the coloring with disjoint red cliques of order and all other edges blue (Chvátal and Harary, as quoted in [KLS21], p. 2), so the content of the problem is the upper bound. The exception is needed, since while the formula gives ; the 1978 source prints its conjecture as "for all " without the exception. Below the range the formula fails badly: lies between and (see Problem 159), far above the linear formula, and [KLS21] Theorem 1.2 gives for and .
Status. The site labels the problem DECIDABLE, which the site defines as resolved up to a finite check. The label is a statement about the shape of what remains, not a theorem; it is recorded as the accepted partial claim page Keevash, Long and Skokan 2021, whose Covers. states the finite check, and the page records what is proved and what remains. A full proof of the identity, closing that check, is given by the OpenAI release's preprint of 25 September 2026 and accepted on the claim page OpenAI 2026 on its Lean proof, which this corpus built, checked for axioms and found identical to the release's comparator challenge; the preprint itself is unrefereed and unreviewed. The derived standing, solved, proved, departs from the site's DECIDABLE by counting that accepted full claim; the refereed partial claims alone leave the finite check open, which is what the label records. Proved, in refereed sources, each an accepted partial claim on its refereed publication alone: the identity for ([BoEr73] Theorem 4, Bondy and Erdős 1973), for when ([Ni05], preprint Theorem 1, Nikiforov 2005) and for with an absolute constant that is not computed ([KLS21] Theorem 1.1), which covers every once exceeds a threshold that the paper does not name; the case is the classical for (quoted from Chartrand and Schuster on p. 47 of [BoEr73]), the cases , , are reported settled for all by the introductions of [Ni05] and [KLS21] (sources not held), and the literature list of [OAI26] (Section 1.1) reports settled for all by Chen, Cheng and Zhang (2008) and, for , the lengths , and settled by papers of 2007--2023 (sources not held). Left by the refereed results: for each of the finitely many with , the cycle lengths with , less the settled cases, so that for the lengths below the threshold of [KLS21] remain: a finite set of pairs whose extent is unknown because is not explicit. No refereed source closes it; the accepted 2026 result closes all of it. The one site comment (1 September 2025) describes the state before the release: reduced to a finitary problem, still open.
Source. erdosproblems.com/551, accessed 2026-09-17: the problem page (DECIDABLE, defined on the page as resolved up to a finite check; source key [EFRS78]; no last-edited date shown), its one-comment discussion thread and its empty proof-claim tab. The site cites [BoEr73], [Ni05] and [KLS21] in its commentary. Cite as: T. F. Bloom, Erdős Problem #551, https://www.erdosproblems.com/551, accessed 2026-09-17.
References.
- [EFRS78] Erdős, P., Faudree, R. J., Rousseau, C. C. and Schelp, R. H., On cycle-complete graph Ramsey numbers. J. Graph Theory 2 (1978), no. 1, 53--64, doi:10.1002/jgt.3190020107; Section 7, printed p. 64. Library home: erdos_1978_cycle_complete_graph_ramsey_numbers.
- [BoEr73] Bondy, J. A. and Erdős, P., Ramsey numbers for cycles in graphs. J. Combinatorial Theory Ser. B 14 (1973), no. 1, 46--54, doi:10.1016/S0095-8956(73)80005-X; Theorem 4, p. 52; Theorem 5, p. 53. Library home: bondy_1973_ramsey_numbers_cycles_graphs; result page Theorem 4.
- [Ni05] Nikiforov, V., The cycle-complete graph Ramsey numbers. Combin. Probab. Comput. 14 (2005), no. 3, 349--370, doi:10.1017/S096354830400642X (published 11 April 2005); arXiv:math/0404501v1 (27 April 2004, 23 pages, "accepted in Comb. Prob. and Comp"). The journal article is paywalled; the preprint's Theorem 1 (p. 2) is the statement cited here, and the journal version numbers its statements differently. Library home: nikiforov_2005_cycle_complete_graph_ramsey_numbers; result page Theorem 1.
- [KLS21] Keevash, P., Long, E. and Skokan, J., Cycle-complete Ramsey numbers. Int. Math. Res. Not. IMRN 2021, no. 1, 275--300, doi:10.1093/imrn/rnz119 (online 10 July 2019; the site's reference gives the pages as 277--302); arXiv:1807.06376v1 (17 July 2018, the only arXiv version); Theorem 1.1, p. 2 of the preprint. Library home: keevash_2021_cycle_complete_ramsey_numbers.
- [ChHa72] Chvátal, V. and Harary, F., Generalized Ramsey theory for graphs, III. Small off-diagonal numbers. Pacific J. Math. 41 (1972), 335--345. The lower bound; not held; quoted here from [KLS21], p. 2.
- [Sch03] Schiermeyer, I., All cycle-complete graph Ramsey numbers . J. Graph Theory 44 (2003), 251--260. The range and the case ; not held; second-hand through [KLS21] (p. 2) and [Ni05] (p. 1).
- Small orders, second-hand through [KLS21] (p. 2, references [24, 43, 52, 8, 44]) and [Ni05] (p. 1), none held: Faudree, R. J. and Schelp, R. H., All Ramsey numbers for cycles in graphs, Discrete Math. 8 (1974), 313--329, and Rosta, V., On a Ramsey type problem of J. A. Bondy and P. Erdős, I and II, J. Combin. Theory Ser. B 15 (1973), 94--120 (); Yang, J. S., Huang, Y. R. and Zhang, K. M., The value of the Ramsey number is (), Australas. J. Combin. 20 (1999), 205--206 (); Bollobás, B., Jayawardene, C. J., Yang, J. S., Huang, Y. R., Rousseau, C. C. and Zhang, K. M., On a conjecture involving cycle-complete graph Ramsey numbers, Australas. J. Combin. 22 (2000), 63--71 (); Schiermeyer, I., The cycle-complete graph Ramsey number , Discuss. Math. Graph Theory 25 (2005), 129--139.
- Exact values for and , second-hand through the literature list of [OAI26] (Section 1.1 and its bibliography), none held: Chen, Y., Cheng, T. C. E. and Zhang, Y., The Ramsey numbers and , European J. Combin. 29 (2008), no. 5, 1337--1352, doi:10.1016/j.ejc.2007.05.007 (, all ); Jaradat, M. M. M. and Alzaleq, B. M. N., The cycle-complete graph Ramsey number , SUT J. Math. 43 (2007), 85--98, and Zhang, Y. and Zhang, K. M., The Ramsey number , Discrete Math. 309 (2009), 1084--1090 (); Bataineh, M. S. A., Jaradat, M. M. M. and Al-Zaleq, L. M. N., The cycle-complete graph Ramsey number , ISRN Algebra 2011, Art. ID 926191 (); Baniabedalruhman, A., The cycle-complete graph Ramsey numbers , for , Jordan J. Math. Stat. 16 (2023), no. 4, 703--718 ().
- [OAI26] OpenAI, Cycle--clique Ramsey numbers. OpenAI Math Release
preprint, 25 September 2026, 41 pages, in the release's folder
preprints/Cycle-clique-Ramsey-numbers-September-25-2026(PDF, pinned); Theorem 1.1 and Section 1.1, p. 2. Unrefereed. Library home: openai_2026_cycle_clique_ramsey_numbers; result page Theorem 1.1. - [KuWa26] Kuang, P. and Wang, Y., An optimal bound for Ramsey goodness of cycles. arXiv:2607.26956 (v1 29 July 2026; v2 31 August 2026). Preprint; abstract only. Lead, recorded below.
- [Ma20] Madarasi, P., The Ramsey number of a long cycle and complete graphs. arXiv:2003.12691 (v2 25 September 2020). Abstract only. Lead, recorded below.
Formalization. Statement only in formal-conjectures; the OpenAI release
carries a Lean proof, built in this corpus (below). The file
ErdosProblems/551.lean
of formal-conjectures, at the pinned commit of its main branch as of 2026-09-17,
declares
erdos_551 : ∀ (k n : ℕ), 3 ≤ n → n ≤ k → ¬(n = 3 ∧ k = 3) → SimpleGraph.graphRamsey (SimpleGraph.cycleGraph k) (SimpleGraph.completeGraph (Fin n)) = (k - 1) * (n - 1) + 1
under category research open, with proof sorry, and the variant
erdos_551.variants.sufficiently_large
(∀ᶠ n : ℕ in atTop, ∀ k : ℕ, n ≤ k → … = (k - 1) * (n - 1) + 1) under
category research solved, also with proof sorry and a docstring crediting
[KLS21]. The community database (teorth/erdosproblems,) records the statement as
formalized since 9 September 2026 and no formal proof; the site's page marks the
statement as formalized. The formal-conjectures file was not built or checked by
this corpus. The OpenAI release's Lean tree, at the revision its claim page
pins, states the theorem as OAI.CycleClique.thm_main and holds a solution
module that proves it; this corpus built thm_main, found its axioms to be
exactly propext, Classical.choice and Quot.sound and its fingerprint
identical to the comparator challenge, and the claim page
OpenAI 2026 records
the files and the statement comparison.
Current assessment
The question (site formulation). The statement above; status DECIDABLE, defined on the page as resolved up to a finite check; source key [EFRS78]. The commentary, in summary, attributes the question to Erdős, Faudree, Rousseau and Schelp and records their two further questions for fixed , the least at which the identity holds and the minimizing ; it credits Bondy and Erdős [BoEr73] with the identity for , Nikiforov [Ni05] with the extension to , and Keevash, Long and Skokan [KLS21] with the range for a constant , hence the conjecture for all large ; and it places the problem as number 18 of the Ramsey theory section of the graphs problem collection. The discussion thread has one comment (1 September 2025) saying that the problem has been reduced to a decidable, finitary question but is still open. The proof-claim tab is empty. The community database record says decidable (last updated 31 August 2025), statement formalized, no formal proof.
Origin. Section 7 of [EFRS78] (printed p. 64) poses two questions about for fixed : "(i) What is the smallest value of such that ? It is conjectured that this formula holds for all ." and "(ii) What value of gives the minimum value of ?" (result page). The printed conjecture has no exception at ; [Ni05] and [KLS21] state it with the exception, as the site does.
What is proved. [BoEr73]
Theorem 4
(printed p. 52): if
, that is, the identity for in the site's letters
(the paper's range is "", the site's commentary writes "");
Theorem 5
(p. 53) gives the general bound . [Ni05]
Theorem 1
(preprint p. 2): if and then
, the identity for and ; its
introduction records the intermediate range of Schiermeyer
and the cases as proved (second-hand), and its concluding
remarks (p. 22) say the method reaches except for one lemma and
that it "seems that with some additional refinement" can be
reached, and conjecture a polynomial threshold (Conjecture 16). [KLS21]
Theorem 1.1
(preprint p. 2): there is with
for and
(logarithms to base ); since for all beyond
a threshold , this proves the identity for every once
, which the site's commentary describes as the conjecture for
all large , and also Nikiforov's Conjecture 16. Their Theorem 1.2 shows
the threshold is tight up to . Acceptance evidence: J. Combinatorial
Theory Ser. B, Combin. Probab. Comput. and IMRN are refereed journals, the
refereed evidence of the three accepted partial claims
Bondy and Erdős 1973,
Nikiforov 2005
and
Keevash, Long and Skokan 2021;
the site's credit under its label DECIDABLE is not reviewed evidence,
since that label settles neither the problem nor a declared part of it.
[Ni05] and [KLS21] are cited from their arXiv preprints, whose journal
texts are not compared. Read depth: claims checked for the four statements
above and for [EFRS78]'s questions; no proof is checked beyond structure.
The finite residue. For each , [Ni05] leaves the cycle lengths (for ) and [KLS21] leaves ; for nothing is left. So the pairs not covered by the three theorems are those with and : finitely many pairs, at most of them for each such . Of these, is classical ( for , on p. 47 of [BoEr73] after Chartrand and Schuster), are reported settled by [Ni05] (p. 1) and [KLS21] (p. 2), from sources not held, and the literature list of [OAI26] (Section 1.1) reports settled for every by Chen, Cheng and Zhang (European J. Combin. 29 (2008)) and, for , the lengths (Jaradat and Alzaleq 2007; Zhang and Zhang 2009), (Bataineh, Jaradat and Al-Zaleq 2011) and (Baniabedalruhman 2023), from sources not held; the citation record of [Ni05] lists some of the same papers by title. The residue is therefore the pairs with in that range of , less those cases, so that for the lengths below the threshold of [KLS21] remain. Its size is unknown: [KLS21] did not compute and write (p. 16) that "with more work it seems that a reasonable value (less than 20, say) can be obtained". No refereed source closes any part of it; the 2026 result below, accepted on its Lean proof, closes all of it. This is the finite check the site's label refers to; the label is kept as the catalog's, and whether "decidable" should stand for a statement that is true for all and unchecked for finitely many is a status question this page records rather than decides.
Closure of the residue (2026). The OpenAI mathematics release's
preprint Cycle--clique Ramsey numbers [OAI26] (25 September 2026), carded at
openai_2026_cycle_clique_ramsey_numbers,
states as its
Theorem 1.1
the identity for every except , with , by a
structural reduction in a minimal counterexample to finite pattern
instances excluded by two exact checkers whose code and deduction traces
accompany the paper
(Proposition 9.1),
and with a Lean statement and solution module in the release's tree. The
release's README states that its manuscripts were produced by an internal OpenAI
model, which it does not name, and that the collection includes results at
different stages of verification, not all with accompanying Lean formalizations;
the claimant is the organization. It is accepted on the claim page
OpenAI 2026 on its
Lean proof: this corpus built OAI.CycleClique.thm_main at the release's pinned
revision, checked its axioms and found it identical to the comparator challenge,
and its statement is the identity for every except together
with . The preprint is unrefereed, with no independent review
known; this corpus has not run its checkers and has checked only its abstract,
introduction and finite-results sections. It postdates the search below. It
closes the residue above and settles the problem.
Adjacent results and leads (not status). The Ramsey-goodness literature proves the same formula for cycles against general graphs with in place of : the abstract of [KuWa26] (arXiv v2,) claims is -good whenever for an absolute constant , resolving a conjecture of Pokrovskiy and Sudakov; for this is a linear threshold in , weaker than [KLS21] for cliques, and the preprint is unrefereed and unread beyond its abstract. [Ma20] (abstract read) generalizes [Ni05] to for with . The small- regime ( fixed, ) is a different problem (Problem 159 for ); a 2025 preprint on odd cycle-complete numbers (arXiv:2511.10641) belongs there.
Search scope. None of the routes below found a source closing the residue, a disproof or a proof claim.
- The site: problem page, discussion thread and proof-claim tab; the community database record; the formal-conjectures file at the pinned commit.
- The primary sources: [EFRS78] printed p. 64, [BoEr73] pp. 46--54, [Ni05] preprint pp. 1--4 and 22 and [KLS21] preprint pp. 1--3 and 16.
- arXiv: the abstract pages of 1807.06376 (one version, no journal
reference) and math/0404501 (one version; "accepted in Comb. Prob. and
Comp"); the API queries
au:Nikiforov AND abs:cycle(twelve records, among them the preprint of [Ni05]),abs:"cycle-complete" AND abs:Ramsey(four records) andabs:Ramsey AND abs:cycle AND abs:"complete graph" AND abs:"(k-1)(n-1)"(two records); the abstracts of 2607.26956, 2606.11174, 2507.11835, 2003.12691, 1807.02313 and 2601.10238. - Crossref: the records of [KLS21] (bibliographic query), [Ni05] (DOI) and [BoEr73] (bibliographic query).
- Semantic Scholar: the citation lists of [KLS21] (21 records) and of the [Ni05] preprint (70 records), scanned by title.
- The publisher's page of [Ni05], which shows the abstract only; the article is paywalled.
Not searched: MathSciNet, zbMATH, Google Scholar, X. Unread: the journal texts of [Ni05] and [KLS21]; [Sch03], [ChHa72] and the small-order papers; the exact-value papers for known by title.
Remaining gaps. (1) The residue is closed only by the 2026 result, on its Lean proof; the manuscript is unrefereed and unreviewed, and no refereed source closes the residue, whose extent as the refereed results leave it still depends on the uncomputed constant of [KLS21]; an explicit or with a source treating the pairs , (for , the lengths ) would give a refereed route. (2) The site's label DECIDABLE stands for a statement that is proved for all and unchecked for finitely many ; whether that label should stand for such a statement is a question this page records rather than decides. (3) Proof coverage is statements only: Theorems 4 and 5 of [BoEr73], Theorem 1 of [Ni05] and Theorem 1.1 of [KLS21] are paged at claims checked, with their proofs read for structure at most; nothing is independently reviewed. (4) The journal versions of [Ni05] and [KLS21] are not compared with the arXiv preprints cited. (5) The formal-conjectures file is a statement, not a proof.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- bondy_1973_ramsey_numbers_cycles_graphs
- bondy_1973_ramsey_numbers_cycles_graphs / theorem_4
- bondy_1973_ramsey_numbers_cycles_graphs / theorem_5
- erdos_1978_cycle_complete_graph_ramsey_numbers
- erdos_1978_cycle_complete_graph_ramsey_numbers / conjecture_p64
- keevash_2021_cycle_complete_ramsey_numbers
- keevash_2021_cycle_complete_ramsey_numbers / theorem_1_1
- nikiforov_2005_cycle_complete_graph_ramsey_numbers
- nikiforov_2005_cycle_complete_graph_ramsey_numbers / conjecture_16
- nikiforov_2005_cycle_complete_graph_ramsey_numbers / theorem_1
- openai_2026_cycle_clique_ramsey_numbers
- openai_2026_cycle_clique_ramsey_numbers / proposition_9_1
- openai_2026_cycle_clique_ramsey_numbers / theorem_1_1