Erdős Problem 625: Chromatic-Cochromatic Gap for Random Graphs

### What is the conjecture

Let $G(n, 1/2)$ denote a random graph on $n$ vertices where each edge appears independently with probability $1/2$. The **chromatic number** $\chi(G)$ is the minimum number of colors needed to color vertices so adjacent vertices have different colors. The **cochromatic number** $\zeta(G)$ is the minimum number of colors needed so each color class forms either a complete subgraph or an independent set.

It is known that almost surely:
$$\frac{n}{2\log_2 n} \leq \zeta(G) \leq \chi(G) \leq \frac{n}{2\log_2 n}(1 + o(1))$$

**Conjecture:** Almost surely, the difference grows unboundedly:
$$\chi(G) - \zeta(G) \to \infty \text{ as } n \to \infty$$

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

**Sources:**
- https://www.erdosproblems.com/625, https://doi.org/10.1002/jgt.3190170309 (Erdős & Gimbel 1993), https://www.cambridge.org/core/books/random-graphs/01A4D4002B07556A6EBD4D4EBC853C15 (Bollobás 1988)

### Prerequisites needed

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

Building blocks (from search results):
- Basic graph theory structures (vertices, edges) available in Mathlib's `SimpleGraph`
- Probability theory framework exists in Mathlib for formalizing random graphs

Missing pieces:
- Formalization of chromatic number χ(G): the minimum coloring function and its properties
- Formalization of cochromatic number ζ(G): the minimum partition into cliques/independent sets and its properties

Rating justification: Core graph objects exist in Mathlib, but chromatic and cochromatic numbers are specialized graph parameters not yet formalized. Defining these requires moderate infrastructure development (defining colorings, partitions with specific structure properties, and establishing the relationship between them), but the underlying mathematical framework is well-established.

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

* ams-05
* ams-60

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