Erdős Problem 62: uncountably infinite chromatic number yet no common infinite subgraphs?

### What is the conjecture

https://www.erdosproblems.com/62

If $G_1,G_2$ are two graphs with chromatic number $\aleph_1$ then must there exist a graph $G$ whose chromatic number is $4$ (or even $\aleph_0$) which is a subgraph of both $G_1$ and $G_2$?

### 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 conjecture statement at https://www.erdosproblems.com/62. Then inspect the repository’s existing formalized conjectures and determine how this graph-theoretic statement should be represented in Lean. Done means the conjecture has been added in the project’s established format and its formalization checks successfully.

Written by the indexing model from the issue text.