An infinite-chromatic graph whose $n$-vertex subgraphs are within $f(n)$ edges of bipartite (Erdős #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? (Equivalently: an infinite-chromatic graph all of whose $n$-vertex subgraphs are within $f(n)$ edge-deletions of containing no odd cycle.) The conjecture asserts this for every function $f(n)\to\infty$; a negative answer would exhibit some $f(n)\to\infty$ for which no such graph exists.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable Lean/Coq preferred, else a full written proof with all steps) that for EVERY function $f(n)\to\infty$ there exists a graph of infinite chromatic number all of whose $n$-vertex subgraphs can be made bipartite by deleting at most $f(n)$ edges — or a proof exhibiting a specific $f(n)\to\infty$ for which no such graph exists. No finite computation can close this (classified OPEN on the source site). ADVANCES: a proof for any function asymptotically smaller than the best known ($f(n)=\epsilon n$, Rödl, as stated in the background) — e.g. $f(n)=o(n)$, $f(n)=n^{1-\delta}$, or the benchmark case $f(n)=\sqrt{n}$; a new obstruction theorem constraining what $f$ can work; a transfer argument between the hypergraph case (known) and the graph case; or a Lean formalization of Rödl's $\epsilon n$ theorem or of the $\aleph_1$ failure. Conditional or consistency-only results must be clearly flagged as such. Deliver the proof file (or formalization artifact) with the construction and its two certifying arguments: infinite chromatic number, and the $f(n)$ near-bipartiteness of all finite subgraphs.