最近几个月，AI 在数学上的进展已经到了令人有些麻木的程度。竞赛成绩早已不再是最值得讨论的事情。长期开放问题被解决或实质推进，新的反例被发现，大规模的证明搜索与形式化验证开始进入真正的研究数学。2026 年 8 月，OpenAI 一次公布了十项数学与理论计算机科学方面的进展，其中一些成果在数学社区看来足以构成传统意义上的重要研究工作。到了 9 月，围绕 Navier–Stokes 千禧年问题的候选解答又把这种冲击推到了大众视野的中央。

Rethlas是北大团队开源的两个Agent集合体，用于辅助数学证明，其中一个Agent负责推理，另一个Agent负责验证想法，整个过程基本是模拟人类数学工作者的工作流（直觉推导+仔细验证）。最近一位北大的数学工作者用Rethlas连发若干篇代数几何方面的文章，即使没有单位距离猜想重磅，但也引起了一些骚动。这件事特殊的地方在于，Rethlas是开源的，只需要对Codex的访问权限即可使用，正好我手里有ChatGPT plus订阅，这两天便花了些时间折腾了一下。