← 返回 PaperDaily 大模型与智能体

5条命令1秒验证，60年数学难题有了机器裁判

数学家们苦苦追寻了60年的Andrews-Curtis猜想，在长度-14的边界上，有一位独立研究者甩出了一套机器可验证的JSON证书——只需5条命令，1秒内就能让电脑成为定理的裁判。这像不像给数学猜想装上了“代码解释器”？想看看数学+代码如何联手攻克前沿难题？这篇论文值得你花一刻钟感受。

龙哥读论文 阅读 3 查看原文
#AI科研 #强化学习 #人工智能
原论文信息如下：
论文标题:
Machine-checkable equivalence certificates at the length-14 Andrews–Curtis frontier 发表日期:
2026年7月 发表单位:
独立研究者（Josep Carreras） 原文链接:
https://arxiv.org/pdf/2607.23611v1.pdf 开源代码链接:
https://github.com/joe-carr-data/ac-certificates 开源数据集链接:
https://doi.org/10.5281/zenodo.21499081

打破数学猜想的验证难题：机器证书登场

数学界有个流传近60年的“老大难”——Andrews-Curtis猜想。简单来说，它问的是：对于一个能用n个生成元和n条关系式定义的“平凡群”（即整个群只有单位元），是否总能通过一系列基本的“Andrews-Curtis移动”（简称AC移动），把这些关系式化简成x₁, x₂, …, xₙ这种标准形式？这个问题连接着低维拓扑、组合群论甚至4维流形，但至今悬而未决。
随着研究的深入，人们发现：在秩为2的情况下，当总关系长度不超过12时，猜想无条件成立；长度为13时，要么平凡，要么等价于那个传说中难以驯服的Akbulut–Kirby表示AK(3)；而到了长度14，情况就变得异常复杂起来。
龙哥在这里插一句，大家可能觉得这有点抽象。你可以把生成元想象成字母，关系式想象成拼写规则。Andrews-Curtis猜想要问的是：给定一套把群“压缩”成平凡群的规则，能不能通过几个特定的“单词游戏”，把它简化到最简单的形式？
而就在2026年7月，一位独立研究者Josep Carreras，就用一种令人信服的方式，向这个前沿发起了冲击。

六个困难表示，四个公开证书

之前，Shehper等人的研究团队（arXiv:2408.15332）用强化学习尝试攻克这个难题，他们报告在Miller–Schupp系列（具体形式为MS(n, w) = ⟨x, y | x⁻¹yⁿxy⁻⁽ⁿ⁺¹⁾, x⁻¹w⟩）中，遇到了六个长度为14的“硬骨头”，其中四个声称等价于AK(3)，剩下两个是“顽固不化”的悬案。但关键问题在于：没有公开任何移动序列（即证书）！
这就像是高考数学压轴题，学霸跟你说“我解出来了”，但就是不写解题步骤，你说你信还是不信？在学术界，没有“解题步骤”（即证书），这种声明只能停留在“声称”阶段。
Carreras的工作，就是给这六个“硬骨头”中，除了两个已经声明的之外，其余四个都补上了详尽的“解题步骤”，并且是以机器可验证的JSON格式给出的。来看看这四份证书有多厉害：
表1：六个疑难表示及状态
图1：六个长度为14的Miller–Schupp表示在文献[15]中的状态，以及本工作给出的定理编号。
简单来说，Carreras证明了：

定理1： P1（即古典候选”Possible Counterexample 1”）与P6等价，证书仅用36个打包步骤（相当于58个经典Gordon组变换）。

定理2： P5与P2等价，证书使用了85个打包步骤（155个经典变换）。

定理3： 将MS(3, yx²y)等价于AK(3)，证书为66个打包步骤（101个经典变换）。

定理4： 将MS(3, y⁻¹x²y⁻¹)等价于AK(3)，证书仅13个打包步骤（22个经典变换），堪称“精悍”。

这些证书的意义在于：它们是GitHub仓库中可直接验证的JSON文件，任何人都能独立地、在不到1秒内重放整个证明过程。
证书验证数据表
表2：五个证书的SHA-256校验码（用于防篡改）、移动步数、以及过程中的最大长度峰值。

最小-最大瓶颈分析揭示对称性不对称

除了给出证书，Carreras还做了一个非常酷的量化分析：在GS-替换图（即由Fagan等人提出的“标准替换移动”构建的图）上，计算了不同表示之间的最小-最大瓶颈距离（dGS）。
这个dGS(S, T)衡量的是：从状态S到状态T，所有可能路径中，路径上状态能量（总关系长度）的最大值的最小值。简单说，就是找一条“最高点最低”的路。
结果非常有意思：

对于MS(3)情况： dGS(MS(3, yx²y), AK(3)) = 19。这意味着在GS图中，连接它们的两条路径，其最高能量点只需要到19（起始总长为14）。这完全解释了为什么定理3和4可以找到相对较短、低消耗的路径。

对于MS(2)情况： dGS(P1, AK(3)) ≥ 27, dGS(P2, AK(3)) ≥ 27, dGS(P1, P2) ≥ 27。这意味着在GS图中，想要连接它们，需要穿越至少27级能量的“高地”。这比MS(3)的情况高了整整8个单位！

这个发现定量地揭示了两个系列之间的巨大差异：为啥MS(3)相对容易攻克，而MS(2)这么难搞——因为在GS图中，它们之间横亘着一条更深的“峡谷”。
瓶颈分析示意图
图2：GS图中不同类之间的最小-最大瓶颈距离分析，展示了MS(3)与AK(3)的路径需要经过能量19，而MS(2)类需要至少27。

代码、证书、验证器全部开源：让可复现成为标配

更值得赞赏的是，Carreras以一己之力，把整套工具链都开源了。这绝对是一个标杆级别的可复现性实践。
你需要的不是数学博士学位，只需要一台电脑、一个终端，跑几条命令：
    # 验证定理1：P1到P6的对称等价
ac_verify.py cert_sym_equiv_orphan1.json --mode=equivalence

# 验证定理2：P5到P2的镜像等价
ac_verify.py cert_idx0_equiv_mirror.json --mode=equivalence

# 验证定理3：MS(3, yx²y) 到 AK(3)
ac_verify.py bottleneck_ak_f3_cert.json --mode=equivalence

# 验证定理4：MS(3, y⁻¹x²y⁻¹) 到 AK(3)
ac_verify.py cert_ms3_yinvx2yinv_equiv_ak3.json --mode=equivalence

# 验证器自检
python selftest_ac.py
    这五条命令，几乎能让任何人在不到1分钟内，验证整篇论文的核心结果。验证器ac_verify.py是用纯Python写的，标准库无外部依赖，整个操作完全透明。
    仓库还包含：

    搜索引擎代码： 用于发现这些路径的Python和C++程序。

    审计工具： 对“Two-Hump”运动发布的AC-19已解集进行成员审计，确保所有六个基准案例确实未被解决。

    完整的运行记录： 所有穷举搜索的输出已冻结，包括6,212,968和13,504,944个规范状态的导出数据。

    验证器自测试
    图3：验证器自测试通过，证明验证器逻辑可靠。

    从Shehper到Carreras：公开性推动信任

    这篇论文最大的贡献，不在于它攻克了一个全新的、宏大的数学难题（虽然MS(3)分支的无疑问化也是一步重要的推进），而在于它建立了一种全新的、基于机器可验证证书的证明与交流范式。
    Shehper等人虽然宣称了四个等价于AK(3)的结果，但因为没有公开证书，它们在学术界始终处于一种“可信度悬空”的状态。而Carreras的工作，通过公开、独立、可验证的证书，把那些声称变成了可被任何人独立复现的“事实”。
    龙哥觉得，这种让电脑充当“数学裁判”的做法，未来很可能会成为处理复杂、计算密集型数学结果的标配。尤其是在涉及大量搜索、自动化推理的领域，一个64字节的SHA-256哈希和一个可执行的验证器，比上千字的文字描述更让人信服。
    这篇论文的附录里还有个很有意思的“负面发现”：Carreras使用了Prover9自动定理证明器，但发现它有个很隐蔽的“陷阱”。默认情况下，当目标是一个析取（“要么成，要么等价于AK(3)”）时，它会把每个析取项都当作独立的证明目标，然后去找所有目标的证明。它会在成功证明两个目标后，却报告“SEARCH FAILED”，因为它还在找剩下的两个！这在输入命令行时，很容易被误读为完全失败。这个发现对做AI搜索的人应该是个非常实用的提醒。

    龙迷三问

    下面是龙哥对于大家可能的一些问题的解答：

    Q1: AC移动到底是什么？AC移动（Andrews–Curtis移动）是四种基本变换：① 把某个关系式替换成它的逆元；② 把某个关系式替换成自身乘以另一个关系式（或它的逆元）；③ 对某个关系式进行共轭变换（即整体乘以一个生成元及其逆元）；④ 关系式的循环移位。只要通过这些操作能把一组关系式化简成x₁, x₂, …, xₙ，就称该表示为AC平凡的。

    Q2: 什么是GS替换图？为什么它跟AC等价不等价？GS图是由Fagan等人（ICML 2026）提出的一种“标准替换移动”图，它把AC移动中的共轭、循环移位等操作抽象成了更简洁的形式（即“标准替换”）。dGS距离只衡量在这个特定图上的瓶颈距离，它不是真正的AC距离。Carreras在论文中明确说明，dGS下界≥27并不代表AC不等价，只是意味着在GS图中找路径会比较“费劲”，需要穿越更高能量的区域。真正的AC等价性证据在于那些JSON证书。

    Q3: 这篇论文解决了Andrews-Curtis猜想吗？没有。它专注于秩2、总长度为14的Miller–Schupp系列中的一小部分（6个具体表示）。它通过证书证明了其中4个与AK(3)等价（从而把剩下两个破解这个猜想的依赖关系，缩减为仅剩最初Shehper等人未公开的两条MS(2)声明）。距离完全解决整个猜想，还有非常漫长的道路要走。

    如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~

    龙哥点评

    论文创新性分数：★★★★☆

    在方法层面，它没有提出新的数学理论，但它首次将“机器可验证证书”作为数学等价证明的核心载体，这一实践创新对领域可复现性有重大推动作用。

    实验合理度：★★★★★

    所有证书均由独立验证器（ac_verify.py）进行严格验证，并提供了SHA-256校验、运行记录和独立的C++引擎交叉验证。不依赖任何黑盒或专有软件，结论完全可复现。

    学术研究价值：★★★★☆

    它将Andrews-Curtis猜想在长度-14前沿的明确、可验证的进展推进了一步。更关键的是，它树立了一面“可验证数学结果”的旗帜，对计算代数、组合群论领域的研究实践有示范意义。

    稳定性：★★★★★

    证书是确定性算法的产物，一旦验证，结果就是100%稳定的。该方法适用于任何AC等价性问题。

    适应性以及泛化能力：★★★☆☆

    该“证书+验证器”的模式具有很强的适应性，可以推广到任何需要计算机辅助证明的等价性问题。但其搜索策略（GS图+瓶颈Dijkstra）目前仅适用于特定搜索图，尚未证明是通用的AC移动搜索方法。

    硬件需求及成本：★★★★★

    验证器只需要任意一台有Python解释器的设备（包括树莓派），能在1秒内运行。搜索过程虽然耗电（穷举了600多万个状态），但都已经在服务器上完成，结果以开源形式提供。

    复现难度：★★★★★

    代码、数据、验证器全部开源，归档在Zenodo并附有DOI，操作脚本只有几行命令，复现几乎没有门槛。

    产品化成熟度：★★★☆☆

    作为数学研究工具，其产品化程度很高——验证器可以作为CI/CD流水线的一部分，自动检查数学论文中声明的可验证性。但作为直接产品，它的受众是数学家，而非大众。

    可能的问题：论文本质上是“可验证的等价性证明”，而未曾“发现”这些证书背后的深层数学结构。它没有解释为什么这些路径存在，只是证明了它们存在。另外，论文对MS(3)分支的“无疑问化”是建立在Shehper等人的两则未公开声明之上的，这多少有点依赖他人的成果。


    主要参考文献

    [1] Andrews, J. J., Curtis, M. L. Free groups and handlebodies. Proc. Amer. Math. Soc. 16(2) (1965), 192–195. doi:10.1090/S0002-9939-1965-0173241-8
    [2] Shehper, A., et al. What makes math problems hard for reinforcement learning: a case study. arXiv:2408.15332, 2024.
    [3] Fagan, L., et al. The Two-Hump Problem: Bridging the Difficulty Gap in Mathematical Reinforcement Learning. ICML 2026, arXiv:2606.21611.
    [4] Carreras, J. Machine-checkable equivalence certificates at the length-14 Andrews–Curtis frontier. arXiv:2607.23611v1, 2026.
    [5] GitHub仓库: https://github.com/joe-carr-data/ac-certificates (tag v1.0)
    [6] Zenodo数据存档: https://doi.org/10.5281/zenodo.21499081 (DOI 10.5281/zenodo.21499081)

    *本文仅代表个人理解及观点，不构成任何论文审核或者项目落地推荐意见，具体以相关组织评审结果为准。欢迎就论文内容交流探讨，理性发言哦～ 想了解更多原文细节的小伙伴，可以点击"阅读原文"，查看更多原论文细节哦！       

    end
    数学猜想都能被机器验证，还有什么不能被证明？快来龙哥读论文粉丝群，与各路高手研讨AI论文、算法前沿，扫码加群开启思辨之旅。
    欢迎加入龙哥读论文粉丝群，扫描下方二维码或者添加龙哥助手微信号加群：kangjinlonghelper。一定要备注：研究方向+地点+学校/公司+昵称（如 图像处理+上海+清华+龙哥），根据格式备注，可更快被通过且邀请进群。
    『龙哥读论文』微信群目前包含：图像处理、大模型及智能体、自动驾驶及机器人、AI医疗及AI金融5个群
    wechat_helper dianzan
    转发文章 微博 X LinkedIn Facebook
    龙哥读论文 · PaperDaily

    本文基于龙哥读论文 PaperDaily 数据库整理，结合论文原文与工程视角进行解读。