Skip to content

Erdős problem 74

Let f(n)→∞f(n)\to \infty possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on nn vertices can be made bipartite by deleting at most f(n)f(n) edges?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

74.lean

Retained formal statement1 of 4

Let f(n)→∞f(n)\to \infty possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on nn vertices can be made bipartite by deleting at most f(n)f(n) edges?

FormalConjectures/ErdosProblems/74.leanErdos74.erdos_744 linesExact file
True ↔  ∀ (f : ℕ → ℕ),    Filter.Tendsto f Filter.atTop Filter.atTop →      ∃ V G, G.chromaticNumber = ⊤ ∧ ∀ (n : ℕ), Erdos74.SimpleGraph.maxSubgraphEdgeDistToBipartite G n ≤ f n
OpenStatement only, no proof