AI 中文总结
本文通过 Lean 4 机器验证，构造了一个四参数无限反例族，证明“墙上的文字 II 猜想 194”即使限制最小度下界也不成立。
AI 中文摘要
对于有限简单图 G，令 α(G) 表示其独立数，并令 l_avg(G) = (1 / |V(G)|) sum_{v in V(G)} α(G[N_G(v)]) 为其开邻域的平均独立数。“墙上的文字 II 猜想 194”断言：每个满足 α(G) <= 1 + l_avg(G) 的 n > 1 个顶点的简单连通图都具有哈密顿路径。我们给出了一个四参数反例族。其主要的两参数子族以等号满足所提出的不等式：对于每对整数 s >= 1 和 t >= 3，它具有 (s + 1)t^2 个顶点，独立数为 t + 1，l_avg(G) = t，最小度为 s，但没有哈密顿路径。这整个无限子族在 Lean 4 中进行了机器检查：一个全称量化定理证明了其阶数、连通性、独立数、平均邻域独立数、最小度、猜想假设以及不可追踪性。因此，没有固定的最小度下界可以修复该猜想。情形 (s,t) = (1,3) 有 18 个顶点，但形式化证书是参数化的，而非仅对该单个图的验证。
英文摘要
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.
Comments6 pages. Lean 4.27.0 certificate for the whole two-parameter equality family and for the formal negation of Conjecture 194. The upstream correction was merged into google-deepmind/formal-conjectures on 7 August 2026 (PR 4542), which now records Conjecture 194 as solved. Lean development archived at doi:10.5281/zenodo.22779981
