Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194
Cameron Beeley
math.CO
Sep 15, 2026 · v1
TL;DR
Lean 4 with Mathlib certifies an infinite parametric family of counterexamples to Written on the Wall II Conjecture 194.
Abstract
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 + l_avg(G) has a Hamiltonian path. We give a four-parameter family of counterexamples. Its principal two-parameter subfamily satisfies the proposed inequality with equality: for every pair of integers s >= 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 number, average neighbourhood independence, minimum degree, conjecture hypothesis, and failure of traceability. Thus no fixed lower bound on the minimum degree repairs the conjecture. The case (s,t) = (1,3) has 18 vertices, but the formal certificate is parametric rather than a verification of that one graph alone.
Problem
Written on the Wall II Conjecture 194 asserts that every simple connected graph on n>1 vertices with alpha(G) <= 1 + l_avg(G) has a Hamiltonian path. The conjecture is catalogued as open in the Formal Conjectures Lean benchmark.
Approach
A four-parameter graph family combining a dense join (controlling local independence numbers) with at least three end cliques attached through single vertices is constructed. The end blocks force distinct path endpoints, obstructing traceability. The principal two-parameter equality subfamily G_{s,t} is formalized directly in Lean 4 on top of Mathlib. A universally quantified theorem family_certificate proves order, connectivity, independence number, average neighbourhood independence, minimum degree, the hypothesis, and non-traceability.
Results
For every s>=1, t>=3, G_{s,t} has (s+1)t^2 vertices, alpha=t+1, l_avg=t, minimum degree s, satisfies the hypothesis with equality, yet has no Hamiltonian path. A separate theorem specialises to the 18-vertex case (s,t)=(1,3), disproving the repository proposition with answer(False); both proof files are free of sorry and compile under Lean 4.27.0.
