Erdős Problem 919

### What is the conjecture

https://www.erdosproblems.com/919

Is there a graph $G$ with vertex set $\omega_2^2$ and chromatic number $\aleph_2$ such that every subgraph whose vertices have a lesser type has chromatic number $\leq \aleph_0$?

What if instead we ask for $G$ to have chromatic number $\aleph_1$?

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start with the linked Erdős Problems page and inspect existing formalized conjectures in the repository to learn the expected Lean statement structure. Formalize the two stated graph-coloring questions, and consider the work complete when both conjecture statements compile in the repository’s Lean checks.

Written by the indexing model from the issue text.