The Ferrers bound for spanning trees in bipartite graphs

TL;DR

This paper proves Ehrenborg's conjecture that connected bipartite graphs have an upper bound on the number of spanning trees based on vertex degrees, with equality characterizing Ferrers graphs, using formal proof in Lean 4.

Contribution

It provides a formal proof of Ehrenborg's conjecture, establishing a precise upper bound for spanning trees in bipartite graphs and characterizing equality cases.

Findings

Confirmed the conjectured upper bound for spanning trees in bipartite graphs.

Characterized Ferrers graphs as the equality case.

Formalized the proof in Lean 4 proof assistant.

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.