Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194
For a finite simple graph G, let alpha(G) denote its independence number and let l_avg(G) = (1 / |V(G)|) sum_{v in V(G)} alpha(G[N_G(v)]) be the average independence number of its open neighbourhoods. Written on the Wall II Conjecture 194 asserts that every simple connected graph on n>1 vertices satisfying alpha(G)<= 1...