Papers With

← All papers
First page of The Ferrers bound for spanning trees in bipartite graphs

The Ferrers bound for spanning trees in bipartite graphs

Boon Suan Ho

math.CO Mar 18, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
Fully formalizes in Lean 4 the proof of Ehrenborg's conjecture on spanning trees in bipartite graphs.
Abstract
We prove Ehrenborg's conjecture that every connected bipartite graph $G$ with parts of size $m$ and $n$ has at most $\frac{1}{mn}\prod_{v\in V(G)} \operatorname{deg}(v)$ spanning trees, and that equality holds if and only if $G$ is a Ferrers graph. The proof is fully formalized in Lean 4.
Problem

Ehrenborg conjectured that every connected bipartite graph G with parts of size m and n has at most (1/mn) times the product of all vertex degrees spanning trees, with equality if and only if G is a Ferrers graph. This bound generalizes known results on spanning tree counts.

Approach

The authors prove Ehrenborg's conjecture by establishing the upper bound on the number of spanning trees in connected bipartite graphs and characterizing the equality case. The proof is fully formalized in Lean 4, providing a machine-checked verification of both the inequality and the characterization of Ferrers graphs as the unique extremal case.

Figure 1. The edges of a Ferrers graph are in direct correspondence with the boxes in a Ferrers diagram. (Reproduced from David Eppstein, “Four open from IPAM” [ 7 ] , 2009, CC BY 4.0 license.)
Results

The conjecture is confirmed: every connected bipartite graph with parts of size m and n satisfies tau(G) <= F(G) = (1/mn) * prod(deg(v)), with equality iff G is a Ferrers graph. The entire proof is formally verified in Lean 4.