Erdős Problem 1111: Anticomplete Sets and Chromatic Number

### What is the conjecture

For a finite graph $G$ with disjoint vertex sets $A$ and $B$ that are anticomplete (no edges between $A$ and $B$), the conjecture states: if $t, c \geq 1$ then there exists $d \geq 1$ such that whenever $\chi(G) \geq d$ and $\omega(G) < t$, there exist anticomplete sets $A', B' \subseteq V(G)$ with $\chi(A') \geq \chi(B') \geq c$, where $\chi(H)$ denotes the chromatic number of the induced subgraph on $H$ and $\omega(G)$ is the clique number of $G$.

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

**Sources:**
- https://www.erdosproblems.com/1111, El Zahar and Erdős [ElEr85], Erdős [Er85b], Nguyen, Scott, and Seymour [NSS24]

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Graph structure basics (vertices, edges, induced subgraphs) are standard in Lean
- Chromatic number and clique number concepts exist in combinatorics literature
- Anticomplete/independent set concepts are foundational

Missing pieces (exactly 2; unclear/absent from search results):
- No direct Mathlib library search results for chromatic number or clique number definitions suitable for this statement
- Existential quantification over graph parameters $d$ requires careful formalization of the relationship between chromatic/clique parameters

Rating justification (1-2 sentences): The statement involves graph colorings and parameterized graph properties that would require developing or importing significant graph-theoretic infrastructure in Lean. While the underlying concepts are standard in mathematics, formalizing chromatic and clique numbers with their precise relationships to induced subgraph decompositions requires substantial new definitions and lemmas in the formal system.

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