PROVED LEANdatabase updated 2025-08-31
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Vertices of the generalised Mycielskian \(M_s(G)\): \(s\) copies of the vertices of \(G\), one per level, and a single apex.
Adjacency of the generalised Mycielskian, before `SimpleGraph.fromRel` packages it as a graph. Two level-`0` vertices are adjacent when the underlying vertices are; a level-`i` vertex and a level-`i + 1` vertex are adjacent when the underlying vertices are; and the apex is adjacent to every vertex on the top level. The relation is already symmetric and irreflexive, so `fromRel` changes nothing about it.
The **generalised Mycielskian** \(M_s(G)\). \(M_2(G)\) is the classical Mycielskian, and \(M_1(G)\) adds a vertex joined to everything.
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. The proof in plby/lean-proofs uses the proof of `erdos_750.variants.stiebitz` linked above. It produces a graph on a `V : Type`, which gives the statement below in any universe by lifting `V`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/750.
NOBODY HAS SENT US AN ATTEMPT YET
If you take a run at this one — with your own AI subscription or without — the guide says how,
and the submission form gets you an honest read of what you found.