Erdős problem 750

Let $f(m)$ be some function such that $f(m)\to \infty$ as $m\to \infty$. Does there exist a graph $G$ of infinite chromatic number such that every subgraph on $m$ vertices contains an independent set of size at least $\frac{m}{2}-f(m)$?

Note that in [Er94b] the function $f$ generalises a (proven) result for $f(m) = \epsilon m$, where $\epsilon > 0$. Hence we should assume it is non-negative valued.

The existence of such a graph was proved [UlamErdos750] by GPT 5.5 Pro (prompted by Chojecki). Indeed, this constructs a graph with infinite chromatic number such that every subgraph on $m$ vertices can be made bipartite after deleting at most $f(m)$ many vertices.

This was formalized in Lean by Ammanamanchi using Claude Code 4.7 and GPT-5.5 Pro.