Erdős Problem 750

References:

• erdosproblems.com/750
• [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.

theorem Erdos750.erdos_750 : True ↔ ∀ (f : ℕ → NNReal), Filter.Tendsto f Filter.atTop Filter.atTop → ∃ (V : Type u_1) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧ ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m → ∃ I ⊆ S, G.IsIndepSet I ∧ ↑m / 2 - f m ≤ ↑I.ncard

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.