又一个百年数学问题被“ AI+外行 ”攻破

luyuanhong

又一个百年数学问题被“ AI+外行 ”攻破

原创  关注前沿科技  量子位  2026 年 9 月 6 日 16:00  北京

鱼羊 发自 凹非寺

量子位 | 公众号 QbitAI

AI ，正在让那些「错位时空」中高悬的有趣科学谜题，迎来解答。

1928 年，在意大利博洛尼亚举行的国际数学家大会上，数学家 Colombo 留下了一道看起来非常简单的行列式题。





问题似乎并不复杂，但当我们翻开历史会有些意外地发现，其中 D≥N-1 ，且 N 为偶数、D 为奇数的情况，在近百年时间里，竟然一直缺少已知证明。

直到今年 8 月份，一篇预印本新论文给出了明确的答案：

det A≠0 ，当且仅当 D≥N-1 ，并且 N 是偶数，或者 D 是偶数。

有意思的是，论文作者实际上并非数学专业出身，也不是这一方向的职业研究者。

而论文中也明确写到：

生成式 AI 系统在识别证明策略和产出初始证明草稿方面发挥了重要作用。

——是 AI 直接找出了证明路线，并生成了初版证明。

证明全程，AI 只用了 48 个小时，写了 2 万行 lean 代码。

目前，这篇预印本论文已经过小范围同行评阅，尚未经过正式同行评审，论文和 Lean 形式化代码均已公开。

错位下的百年数学问题

在详细探讨 AI 在这项工作中的贡献前，我们还是先来拆解一下问题本身。

在问题被提出的最初，这并不是一个孤立的矩阵问题，而是一个偏微分方程问题：

一个双曲方程的解，如果在若干特征线上给定边界值，什么时候能够被唯一确定？

经过展开，这个问题可以归结为一族非常具体的矩阵，即

  。

意大利数学家 Bonaparte Colombo 发现，当矩阵阶数 N 为偶数、xi 两两不同时，问题的关键之一是：当整数 D≥N-1 时，这个矩阵的行列式是否总是不为零。

有些戏剧性的是，这个问题在 1928 年被提出，但实际上适合于解决这个问题的技术——样条恒等式和系统的全正性理论等，直到 20 世纪七八十年代，才逐渐成熟起来。

也就是说，在 Colombo 提出问题后的 50 年间，这个问题基本上处于一个没有趁手工具来解答的状态。



1986 年，Dyn 、Goodman 和 Micchelli 在研究另一类距离矩阵时，顺手解决了这个问题的偶数次幂情况。即，当 D≥N-1 且 D 为偶数时，矩阵 A 行列式总是不为 0 。

但偶数阶矩阵对应的奇指数部分，仍然遗留了下来。

2026 年，浙江大学人工智能方向博士生、无界 AI 联合创始人马千里，在北大董彬教授发起的 ICMConjectures 项目中，发现了这个问题。

ICMConjectures 是一个 AI for Math 开放数学问题库，目前已经整理出 2898 个仍未完全解决的数学猜想或开放问题，覆盖 18 个数学大领域。

这位近来沉浸于 AI4S 研究的 AI 创业者向量子位谈及了他的初衷：

我一开始关心的是物理和材料领域，但后来发现这些领域往往存在很多争议。相比之下，数学的答案是相对可验证的。

AI + 数学的优势在于，我把这个问题做出来，用 Lean 完成形式化验证，即使我不是职业数学研究者，结果也不会受到太多质疑。

于是，诞生时苦无工具的 Colombo 问题，现在又和最前沿的 AI 技术，关联了起来。

一种 AI 辅助数学研究的新方式

单从论文来看，其实最后的答案跟题面本身一样简短：

把行列式改写成 Pfaffian —— Pfaffian 的平方等于矩阵行列式，即 detA=Pf(A)^2 。

接着把 Pfaffian 变成一个积分，证明积分里的样条行列式非负，最后找出一块严格为正的区域。

复杂的数学证明我们暂且不展开，更值得分享的，是论文作者马千里记录下的整个研究过程。

8 条证明路线

在和浙大于飞教授讨论并选定研究题目之后，1 天之内，马千里就借助 AI 找到了后来写进论文里的核心证明路线。

当然，不是说把问题直接丢给 Chatbot ，敲几个 prompt ，答案就汩汩涌出了。

马千里组建了一支由 GPT-5.6 、Fable 5 和 DeepSeek 等多个 AI 组成的研究团队，让不同的模型来负责不同的工作：

GPT-5.6 查文献，Fable 5 对证明结果做挑刺审核，DeepSeek 做 Lean 形式化证明……

为了更好地把智能体放在一起统一管理，并针对数学问题来配备数学工具，无界AI团队还专门做了一个智能体平台—— WUJIE AIAGENT 。

在这套科研 Agent 系统中，无界 AI 把原本给人使用的数学、计算、数据工具重新适配给 Agent ，并由一个上层 Agent 调度不同模型和子 Agent ：核心长程任务交给更强的模型，可拆分的形式证明交给成本更低的模型，还有独立红队负责找错。人仍然处在最上层，决定研究路径、算力分配。



AI 前后琢磨出了 8 条不同的证明路线。

不过不是每一种思路都值得尝试：有的路线比较直接，但预计需要很大的计算量；有的路线概念漂亮，却在关键环节缺少可以验证的桥梁；还有一些路线看起来成功概率较低，很快就被停止。

每出现一条新路线，AI 系统在尝试证明之外，也会同步评估这条路线目前的优势、缺点、可能遇到的障碍，并给出是否值得继续投入计算资源的建议。

但最后的决策，马千里认为还是要有人来把控：AI 给出的可能性越多，选择反而越重要。

人的一部分工作可能会从“亲手推导每一步”，转向另一类任务：设计搜索，分配资源，判断失败，比较路线，并决定什么时候值得继续。

他把人的判断归结为三个层次：

● 第一层：选什么问题。从大量公开问题中，先判断哪些问题适合当前AI能力、又适合形式化验证。

● 第二层：哪些路线值得继续。AI可以快速生成很多可能性，但需要持续比较成功概率、数学缺口和计算成本。

● 第三层：什么结果值得相信并公开。最终仍然需要形式验证、人工审阅，并接受数学共同体的公开检查。

最终，这项研究形成的 Lean 形式化代码规模约 2 万行。

像人一样，AI 也会失败

有意思的一个小插曲是，这次 AI 解决 Colombo 问题，花费最多时间的环节，其实最后导向的是一个失败的结果。

马千里自己调侃说：

就像拼多多一样，永远觉得砍一刀就能出成果了，但是砍一刀之后还要砍一刀，99% 之后还有 99.9% ，而且越到最后越难，AI 也容易在最后的环节钻牛角尖。



从表格中可以看到，在这项研究中非常关键的 Beta-de Bruijn 恒等式，花费的时间仅 43 分钟。

Beta–de Bruijn 恒等式把 Pfaffian 的符号问题，翻译成了样条行列式的正性问题。前者充满正负抵消，后者却可以借助全非负理论逐块控制。可以说是这个 Colombo 问题能被证明的核心一环。



走到这一步，马千里感觉已经看到了胜利的曙光。但接下来的 11 个小时，AI 却在 p=m-1 这条看似美好的路径上越证明越复杂……越走越远……走远了……

这条路并不是一开始就表现得像死路，恰恰相反，它一路都在不断给出“好消息”。但事实却是，这条路线一共留下了 141 项可核验产物、超过 4.7 万行文本和代码，用时约 11 小时 17 分钟，却始终没能收敛成一个可以覆盖任意规模的统一证明。

核心还是 AI 会被局部进展“奖励”，只要一条路线还能不断产出一点新结果，AI 就很容易继续往这个方向深挖。哪怕边际收益已经越来越低，它还是会试图把最后那一点缺口补上。

人类在这时介入了：马千里决定喊停 p=m-1 这条路线。

而真正的突破，恰恰来自这一次“放弃”。

AI 把目标降到了 p=m-2 ，结果发现：在 p=m-1 时还彼此纠缠的支撑关系，到了 p=m-2 突然变得规整起来。每一列可能非零的位置变成连续区间，而且这些区间会随着列的移动有序推进。

又跑了 2 小时 23 分之后，智能手表开始给马千里报警心跳过快了：证明成了。

最后一步是完成 Lean 形式化验证。一方面是对 AI 的证明初稿进行计算机验证，另一方面可以提高外部读者复核的可信度和效率。

48 小时，2 万行代码落地，非数学研究员马千里的第一篇专业数学论文，最核心的部分跑通了。

One More Thing

这样一项新研究，与其说是“ AI一天时间自动证明了一道百年数学题”，更值得关注的部分，其实在于 AI 辅助科学探索的范式本身。

包括陶哲轩在内的数学家都承认，AI 正在改变包括数学在内的基础科学的研究方式。

作为一名 AI 博士生，也作为一名 AI 创业者，马千里正在亲身实践这种人与 AI 的合作的科研新模式。他还分享了一个有趣的细节。

当他把自己和 AI 合作完成的成果分享出去时，很多数学家的第一反应是：发过来自己细分领域里那些一直没有很好被解决的问题，直接问他能不能让 AI 试一试。

大部分懂数学的人还是没有那么懂 AI ，懂 AI 的人没有那么懂数学。

他坦言，现阶段对很多研究者来说，对 AI 、对 Agent 的使用并不充分，“第一步不是研究复杂的 Prompt 技巧，而是先用对工具”。

以创业者的身份来说，马千里认为这其中的机会在于：

帮助科学家们去做更适合于科研场景的 Harness 。

进一步，在 AI 越来越会串联起一切寻找答案之后，帮助科学家们实现研究范式的转化：

怎么问问题？什么时候继续问问题？什么时候，又应该换一个问题。

量子位