Erdős Problem #73

Let \(k\ge 0\). Let \(G\) be a graph such that every subgraph \(H\) contains an independent set of size \(\ge (n-k)/2\), where \(n\) is the number of vertices of \(H\). Must \(G\) be the union of a bipartite graph and \(O_k(1)\) many vertices? Proved by Reed [Re99]. The linked formal proof (Alexeev and Codex, following Reed's mangoes-and-blueberries argument) states the hypothesis as `∀ H : G.Subgraph, H.verts.ncard ≤ 2 * H.coe.indepNum + k` and the conclusion as `(G.induce Dᶜ).IsBipartite`, for graphs on `Fin n` (and, equivalently, on any finite vertex type); this implies the statement below.