Lean-Certified Infinite 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.
Related
- An infinite family of counterexamples to the Polycirculant Conjecture
- An infinite family of counterexamples to Goss's conjecture on L-functions of cyclotomic function fields
- Disproving the Petersen Coloring Conjecture: Theoretical Analysis and an Infinite Family of Counterexamples
- Infinite Families of Counterexamples to a Conjecture of Liu and Qian and a Refined Inverse Theorem for Restricted Sumsets in ℤp
- Unique Normal Forms: Proof-Graph Counterexamples, Infinite-Carrier Certificates, and Confluence Repair
BibTeX
@misc{beeley2026leancertified,
title = {{Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194}},
author = {Cameron Beeley},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.19195},
eprint = {2609.19195},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.19195},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Lean-Certified Infinite Counterexamples to Written on the Wall II Conjecture 194
AU - Cameron Beeley
PY - 2026
DA - 2026/09/15
PB - arXiv
DO - 10.48550/arxiv.2609.19195
UR - https://arxiv.org/abs/2609.19195
AB - 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.
ER -