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

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

当整数 N ≥ 2 且 D ≥ 1，取 N 个互不相同的实数 x1，…，xN，

对于，什么时候，这个矩阵的行列式不等于 0？

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

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

，当且仅当 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 越来越会串联起一切寻找答案之后，帮助科学家们实现研究范式的转化：

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

一键三连「点赞」「转发」「小心心」

欢迎在评论区留下你的想法！

—  完  —

点亮星标

科技前沿进展每日见