Erdős Problem 556: Ramsey Number R(C_n;3) ≤ 4n−3

### What is the conjecture

Let $K_m$ denote the complete graph on $m$ vertices, and let $C_n$ denote the cycle graph with $n$ vertices. We define $R(C_n; 3)$ as the smallest positive integer $m$ such that every 3-coloring of the edges of $K_m$ contains a monochromatic copy of $C_n$.

**Conjecture:** For all positive integers $n$, we have
$$R(C_n; 3) \leq 4n - 3.$$

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/556

### Prerequisites needed

**Formalizability Rating:** 2.5/5 (0 is best) (as of 2026-02-03)

Building blocks (1-3; from search results):
- Basic graph structures exist in Mathlib (vertices, edges, complete graphs)
- Finitary and combinatorial objects are well-developed

Missing pieces (exactly 2; unclear/absent from search results):
- Ramsey number framework (formal definition of $R(G; k)$ for graphs and number of colors)
- Edge coloring formalization (systematic treatment of $k$-colorings of edges as a Ramsey-theoretic concept)

Rating justification (1-2 sentences): Moderate foundational infrastructure is needed. While basic graph theory exists in Mathlib, the entire Ramsey number system and the formal theory of edge colorings in the Ramsey sense would need to be developed from scratch.

### [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)