Erdős Problem 1156: Chromatic Number Concentration in Random Graphs

### What is the conjecture

Let $G(n, 1/2)$ be a random graph on $n$ vertices where each edge appears independently with probability $1/2$. The question concerns the concentration of the chromatic number $\chi(G)$.

**Question 1:** Does there exist a constant $C$ such that $\chi(G)$ is almost surely concentrated within at most $C$ values? That is, does $\max \chi(G) - \min \chi(G) \le C$ hold almost surely for some fixed $C$?

**Question 2:** For any sufficiently slowly growing function $\omega(n) \to \infty$, does there exist a function $f(n)$ such that
$$\Pr[|\chi(G) - f(n)| < \omega(n)] < \tfrac{1}{2}$$
for all sufficiently large $n$?

The problem asks whether the chromatic number exhibits a strong concentration (within a constant) or whether every possible concentration window of slowly growing width has probability less than $1/2$.

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

**Sources:**
- https://www.erdosproblems.com/1156, https://en.wikipedia.org/wiki/Chromatic_number, https://en.wikipedia.org/wiki/Random_graph

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Graph structures and chromatic number are not directly in Mathlib; would need a graph library or custom definition of chromatic number as the minimum number of colors needed for a proper vertex coloring.
- Probability theory (Mathlib has `ProbabilityTheory`) can handle the random graph model $G(n, 1/2)$ as a probability space.

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of the chromatic number for finite graphs and its properties in a computable or measurable setting.
- Definition and theory of random graphs $G(n, p)$ as a probability space, including measurability of $\chi(G)$ as a random variable.

Rating justification (1-2 sentences): The statement requires non-trivial definitions of graphs, chromatic number, and random graph models that are not readily available in Mathlib's core. While probability theory exists in Mathlib, building the necessary graph-theoretic infrastructure would require moderate new theory development.

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