Erdős Problem 19: Chromatic number of edge-disjoint complete graphs; Erdős-Faber-Lovász Conjecture

### What is the conjecture

If $G$ is an edge-disjoint union of $n$ copies of the complete graph $K_n$, then the chromatic number $\chi(G) = n$. Here, an edge-disjoint union means the $n$ copies of $K_n$ share no common edges, and $\chi(G)$ is the minimum number of colors needed to color the vertices of $G$ such that no two adjacent vertices have the same color.

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

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

### Prerequisites needed

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

Building blocks (1-3; from search results):
- `SimpleGraph` type and basic graph operations in Mathlib
- `CompleteGraph` or ability to construct complete graphs
- Fintype for finite structures

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of chromatic number χ(G) and its properties
- Formalization of edge-disjoint union construction for graphs

Rating justification: The statement itself is straightforward once chromatic number and edge-disjoint union decompositions are available. However, the search found no existing Mathlib definitions for chromatic number or these specific graph operations, requiring moderate new infrastructure (definitions and basic lemmas) to state the conjecture formally.

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