Erdős problem 74
Let possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on vertices can be made bipartite by deleting at most edges?
Sources
FormalConjectures/ErdosProblems/
74.lean
Retained formal statement
The set of minimum edge distances to bipartite for subgraphs of size n is bounded above. A graph on n vertices has at most n choose 2 edges, and deleting all of them makes the graph bipartite, providing a straightforward upper bound.
∀ {V : Type u} (G : SimpleGraph V) (n : ℕ), BddAbove (Erdos74.SimpleGraph.subgraphEdgeDistsToBipartite G n)TestStatement only, no proof