For every finite simple connected graph G=(V,E), let N_G(v) denote the neighborhood of v, let alpha(G[N_G(v)]) be the independence number of the subgraph induced by N_G(v), and define the average local independence by operatornameAvgInd(G)=frac1|V|∑_v∈ Valpha(G[N_G(v)]). Let L_s(G) be the maximum number of leaves in a spanning tree of G. Then 2 bigl(operatornameAvgInd(G)-1 bigr)≤ L_s(G); equivalently, in the formalized notation, 2 bigl(G.operatornameaverageIndepNeighbors-1 bigr)≤ G.Ls.

Written on the Wall II, Conjecture 2

For every finite simple connected graph $G=(V,E)$ , let $N_G(v)$ denote the neighborhood of $v$ , let $\alpha(G[N_G(v)])$ be the independence number of the subgraph induced by $N_G(v)$ , and define the average local independence by $\operatorname{AvgInd}(G)=\frac{1}{|V|}\sum_{v\in V}\alpha(G[N_G(v)])$ . Let $L_s(G)$ be the maximum number of leaves in a spanning tree of $G$ . Then $2\bigl(\operatorname{AvgInd}(G)-1\bigr)\le L_s(G)$ ; equivalently, in the formalized notation, $2\bigl(G.\operatorname{averageIndepNeighbors}-1\bigr)\le G.Ls$ .

Progress summary

Solved

A machine-checked record and a recent paper claim the conjecture is solved, but required review means the result is not yet settled.

The conjecture asserts a graph-theoretic lower bound relating the maximum number of leaves in a spanning tree to average local independence. A paper identifies this as the long-standing conjecture listed in Written on the Wall II, though it also records a different numbering in a later source.

Recent developments, July–August 2026

A paper updated in July 2026 claims a proof via a triangle-free spanning subgraph, a degree-square argument, and extension to a spanning tree; balanced complete bipartite graphs give sharpness.
On August 19, 2026, a public formalization record reported the encoded statement solved in Lean with a passing production verifier. The record explicitly says normal maintainer review remains required.

Current status (as of August 2026): The encoded Lean statement reportedly passes verification and a paper claims the inequality, but independent mathematical confirmation and maintainer review remain outstanding.

ClaudeAnthropicsolved2026-08-19evidence
A WOWII conjecture is formally marked solved

Sources

Sources & referencesView supporting material

Primary source

GitHub

Additional references

Written on the Wall II Conjecture 2 closing record — GitHub

combinatorics formal-methods

2 days ago