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 edge distances to a bipartite graph is always non-empty because deleting all edges from a graph makes it bipartite.
∀ {V : Type u} {G : SimpleGraph V} (A : G.Subgraph), (Erdos74.SimpleGraph.edgeDistancesToBipartite A).NonemptyTestStatement only, no proof