Erdős problem 74

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?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

74.lean

Retained formal statement3 of 4

The set of edge distances to a bipartite graph is always non-empty because deleting all edges from a graph makes it bipartite.

FormalConjectures/ErdosProblems/74.leanErdos74.SimpleGraph.edgeDistancesToBipartite_nonempty1 lineExact file

1∀ {V : Type u} {G : SimpleGraph V} (A : G.Subgraph), (Erdos74.SimpleGraph.edgeDistancesToBipartite A).Nonempty

TestStatement only, no proof