AI 生成两类图 acyclic polynomial 单峰性反例：230 顶点二部图与根全在左半平面的稳定多项式，均报告 Lean 核验

YURAN XIU 于 10 月 18 日发布相互关联的两项图多项式构造（Hexagon 2610.00325v1 与 2610.00326v1），分别回答 Barton–Brown–Pike 的两个问题：一项构造 K46 与三个 P3 的 join，得到系数非单峰、但全部复根实部严格为负的 acyclic polynomial；另一项给出 230 顶点二部图，其 induced-forest 计数多项式在高次数区间先下降再上升。作者在两篇摘要中报告通过 Lean 验证图到多项式的恒等式、精确不等式及第一例中的有理 Lyapunov 稳定性证书。两项均标注 primarily AI-generated / human understanding no parts；为避免相邻同一主题重复灌水，以单个系列里程碑报道，关联论文 https://hexagonmath.org/2610.00326v1。