The board / graph theory / #74
Erdős Problem #74
DISPROVED LEANdatabase updated 2026-09-03
The statement as posed is false. 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).
For a given subgraph `A`, this is the set of all numbers `k` such that `A` can be made bipartite by deleting `k` edges.
The minimum number of edges that must be deleted from a subgraph `A` to make it bipartite.
For a graph `G` and a number `n`, this is the set of `minEdgeDistToBipartite A` for all induced subgraphs `A` of `G` on `n` vertices.
Let \(f(n)\to \infty\) possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on \(n\) vertices can be made bipartite by deleting at most \(f(n)\) edges? The answer is no. A machine-checked disproof constructs a function \(f(n) \to \infty\) for which every graph satisfying this local deletion bound has finite chromatic number.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/74.Prize$500
Topicsgraph theory, chromatic number, cycles
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/74
Attempts
submit one →A reduction plus a conditional construction — no resolution. Open.
NO PROGRESS