机器验证数学证明新进展
kevrussell · x · 2026-07-11
这条引用介绍了一篇新的数学结果：在对偶 kissing configuration 问题中，R¹¹ 和 R¹² 的点数上界分别不能超过 **820** 和 **1,228**。 作者强调这套方法有两个特点： - 能在这些维度上给出比“平分上界”更紧的界。 - 同一条流水线还能**精确复现**经典的 sharp 值，如 **E₈ 对应 120**、**D₄ 对应 12**。 技术上，这是一套“**完全有理数精确算术**”的 Delsarte 线性规划方法： - 使用有理乘子 - 用 Sturm root-counting 在 ℚ 上处理根计数 - 认证路径中不使用浮点数 作者还给出可复现实验方式：克隆仓库后运行 `make verify`，验证器可在几秒内从原始系数重建定理。文中称这是该系列第五篇机器验证笔记，并附 DOI。