theorem WrittenOnTheWallII.GraphConjecture58.conjecture58 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (hG : G.Connected) : ↑⌈G.b / G.l_avg⌉₊ ≤ G.f

WOWII Conjecture 58

For a connected graph G, the size f(G) of a largest induced forest satisfies f(G) ≥ ceil( b(G) / average l(v) ) where b(G) is the largest induced bipartite subgraph and l(v) is the independence number of G.neighborSet v.