Ramsey Number R(5,5) and other Ramsey Number Values

### 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:**
- https://oeis.org/A212954, https://mathworld.wolfram.com/RamseyNumber.html, https://gilkalai.wordpress.com/2017/03/29/r55-%E2%89%A4-48/, https://ajc.maths.uq.edu.au/pdf/5/ocr-ajc-v5-p13.pdf, https://math.mit.edu/~apost/courses/18.204_2018/ramsey-numbers.pdf

### 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.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)