实心网格图哈密顿路径获多项式算法及Lean验证

研究者 zzyzek 发布了一个判定实心网格图中任意两个不同点 s、t 之间是否存在哈密顿路径的多项式时间算法，并在 Lean 4 与 Mathlib 中证明了其正确性和多项式步数上界。该定理针对给定端点 s、t 的路径；端点自由的情形可通过枚举所有点对得到。 作者称，实现代码本身未经形式化验证。zzyzek 还表示，项目几乎全部工作由 Claude（Opus 5.5）完成，包括算法、论文、参考实现、演示、Lean 4 证明和讲解视频。

AI 根据报道生成 · 57 分钟前更新

还没有足够的连续观测数据，暂不绘制趋势。