{"id":"arxiv/2609.19195","url":"https://arxiv.org/abs/2609.19195","tags":["math.CO"],"score":0,"title":"Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194","domain":"math.CO","source":"arxiv","authors":["Cameron Beeley"],"reviews":0,"subject":"math.CO","summary":"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 and t >= 3 it has (s + 1)t^2 vertices, independence number t + 1, l_avg(G) = t, and minimum degree s, but has no Hamiltonian path. This entire infinite subfamily is machine-checked in Lean 4: one universally quantified theorem certifies its order, connectivity, independence…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-15","reactions":{}}