Paths maximize the expected range of graph-indexed random walks
Yinfeng Zhu
math.CO
Sep 17, 2026 · v1
math.PR
TL;DR
The main combinatorial results (BHM and LNR expectation conjectures on graph-indexed random walks) were formalized and checked in Lean 4.
Abstract
We prove that a path maximizes the expected range of a uniformly chosen graph homomorphism into the integers, with one vertex pinned at zero, among all connected bipartite graphs of the same order. This establishes the expectation form of the Benjamini–Häggström–Mossel conjecture. The proof restricts and rescales a homomorphism on each bipartition class, then contracts the edges on which the resulting height function is constant. A quantitative estimate for the rank of these zero edges compensates for a parity term in the expected range of a simple random walk, allowing an induction on the number of vertices. We then prove that the BHM inequality implies the Loebl–Ne\v set\v ril–Reed inequality for uniformly chosen integer 1-Lipschitz functions on arbitrary connected graphs, and hence obtain the LNR conjecture as a corollary of BHM. The proof was obtained through interaction with OpenAI GPT-6 Astra and verified by the author. The main results have also been formalized and checked in Lean 4.
Problem
The Benjamini–Häggström–Mossel conjecture asserts that a path maximizes the expected range of a uniformly chosen graph homomorphism into the integers among connected bipartite graphs of the same order. A related conjecture by Loebl, Nešetřil, and Reed concerns the lazy (1-Lipschitz) model.
Approach
The proof restricts and rescales a homomorphism on each bipartition class, then contracts edges where the resulting height function is constant. A quantitative estimate for the rank of these zero edges compensates for a parity term, enabling an induction on the number of vertices. A switching argument bounds forest probabilities, and the BHM inequality is shown to imply the LNR inequality. The results were formalized and verified in Lean 4.
Results
The expectation form of the BHM conjecture is established for all connected bipartite graphs, and the LNR expectation conjecture follows as a corollary, with strict inequality when the graph contains a cycle.
