What is the conjecture
The Ramsey number $R(5,5)$ is defined as the smallest positive integer $n$ such that every 2-coloring of the edges of the complete graph $K_n$ contains either a monochromatic clique of 5 vertices or a monochromatic independent set of 5 vertices. Equivalently, for any graph $G$ on $n$ vertices, either $G$ or its complement $\overline{G}$ contains a clique of size 5. The exact value of $R(5,5)$ remains unknown, but it is bounded: $43 \leq R(5,5) \leq 48$.
Also add conjectures for other small values.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 1/5 (0 is best) (as of 2026-02-19)
Building blocks (from search results):
SimpleGraph and complete graphs from Mathlib.Combinatorics.SimpleGraph- Graph coloring definitions and 2-coloring concepts
- Cliques and independent sets in SimpleGraph theory
Missing pieces:
- Formal definition of Ramsey number as a minimum function for this specific case
- Lean statements of the established bounds (43 ≤ R(5,5) ≤ 48)
Rating justification: The core graph-theoretic concepts needed to state the conjecture are available in Mathlib. Formalizing the statement primarily requires packaging existing definitions (complete graphs, colorings, cliques, independent sets) into a statement about the Ramsey number bounds; no major new foundational infrastructure is needed.
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link
What is the conjecture
The Ramsey number$R(5,5)$ is defined as the smallest positive integer $n$ such that every 2-coloring of the edges of the complete graph $K_n$ contains either a monochromatic clique of 5 vertices or a monochromatic independent set of 5 vertices. Equivalently, for any graph $G$ on $n$ vertices, either $G$ or its complement $\overline{G}$ contains a clique of size 5. The exact value of $R(5,5)$ remains unknown, but it is bounded: $43 \leq R(5,5) \leq 48$ .
Also add conjectures for other small values.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 1/5 (0 is best) (as of 2026-02-19)
Building blocks (from search results):
SimpleGraphand complete graphs from Mathlib.Combinatorics.SimpleGraphMissing pieces:
Rating justification: The core graph-theoretic concepts needed to state the conjecture are available in Mathlib. Formalizing the statement primarily requires packaging existing definitions (complete graphs, colorings, cliques, independent sets) into a statement about the Ramsey number bounds; no major new foundational infrastructure is needed.
AMS categories
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link