论文证明路径结构最大化图索引随机游走范围

这篇论文证明了在所有相同节点数的连通二分图中，路径结构能最大化均匀选择的图同态到整数的期望范围。研究通过限制和缩放同态在每个二分部分类，然后收缩结果高度函数恒定的边，并给出零边秩的定量估计来补偿奇偶项，从而对节点数进行归纳证明。该证明通过OpenAI GPT-6 Astra的交互完成，并在Lean~4中形式化验证。