论文证明路径结构最大化图索引随机游走范围
Paths maximize the expected range of graph-indexed random walks
这是篇挺硬核的数学证明论文，作者用AI辅助证明了关于图同态的BHM猜想，对图论和概率论研究者可能有参考价值。
这篇论文证明了在所有相同节点数的连通二分图中，路径结构能最大化均匀选择的图同态到整数的期望范围。研究通过限制和缩放同态在每个二分部分类，然后收缩结果高度函数恒定的边，并给出零边秩的定量估计来补偿奇偶项，从而对节点数进行归纳证明。该证明通过OpenAI GPT-6 Astra的交互完成，并在Lean~4中形式化验证。
Paths maximize the expected range of graph-indexed random walks
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.
