Spanning-tree leaf bounds from average local independence

For a finite simple connected graph, let L_S(G) be the largest leaf count in a spanning tree and ℓ(G) its average neighborhood independence number. Must L_S(G)≥2(ℓ(G)−1)?

Why it matters and what counts as progress

Why it matters: The inequality connects local independent sets with globally branching spanning trees.

What counts as progress: A proof for every connected simple graph, a stronger bound or a graph violating the stated inequality.

How the problem developed

1996 · Open conjecture [1]
Graffiti.pc Recorded Conjecture 2: the spanning-tree leaf number of a finite connected graph is at least twice its average neighborhood independence number minus two.
27 Jul 2026 · Proof [1]
Yanmohan Wang, Tianyue Dai and Rui Tong Proved the 1996 inequality for finite simple connected graphs and showed the bound is sharp for balanced complete bipartite graphs.

AI contribution

Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri

For every finite simple connected graph G, the maximum number L_S(G) of leaves in a spanning tree is at least 2(ℓ(G)−1), where ℓ(G) is the average local independence number.

AI involvementAI-autonomous

ImportanceNotable

Technical verificationFormal (Lean 4)

Human understandingFull