有个数学问题，搁置了12年。

不是没人看，是真的没人解得出来。

但是北大的AI，上周把它解出来了。

更要命的是，

北大的AI还丧心病狂的把过程转化为 19,000 行 Lean 4 形式化代码（专门用来“写数学证明、验证真理”的编程语言），用底层微内核的严酷逻辑，把证明过程一行一行锁死，杜绝了任何人类自认为理所应当的漏洞。

北京大学BICMR校园的内部庭院

一道搁置了12年的问题

2014年，美国爱荷华大学数学家Anderson提出了一个数学猜想：

在交换代数里，有一类叫“局部环”的数学结构。

他问：一个满足“弱拟完备”的环，是否会自动升格，满足更为严苛的“拟完备”强条件？

通俗点说：

弱拟完备就像“每个小区都有水喝”——基础条件满足；

拟完备则是“所有小区不仅有水，而且水压、水管、水龙头全都一模一样标准化”。

Anderson问的是：只要有水，系统会不会自动变成完美工程？

答案是：不会。AI找到了反例——有的地方有水，但水压就是参差不齐。

这个问题看起来简单，但12年过去，没人给出答案。

不是没人试过。

是这个问题的反例，线索都散落在各种交叉复杂的文献中。哪怕是最顶尖的学者，也很难同时调动局部环结构与代数拓扑工具，瞬间建立起跨越数十年的直觉跳跃。

北大团队给AI的第一个任务：找答案。

AI系统里有个叫Rethlas的智能体，专门负责数学推理。

它内置了一个检索引擎，覆盖数千万条数学文献和定理。

它开始搜索。

搜着搜着，它找到了一篇2006年的老论文——Jensen写的，研究整环完备化。

这篇论文，在数学界某个角落安静地躺了20年。（实在是没人关注...）

AI不一样。它全都看过。

它发现：Jensen 2006年的一个技术性结论，可以用来构造Anderson猜想的反例——答案是否定的，那个“弱条件”并不能推出“强条件”。

2014年提出的问题，2006年就有人给出答案了！结果12年来，这个答案就在那里。没人看见。

# 北大团队给AI的第二个任务：自己纠错

北大团队给这个系统加了另一个形式化验证AI智能体，Archon。

内部还有两个子智能体配合：

Plan Agent：规划任务分解，避免上下文污染
Lean Agent：执行形式化，逐个消除占位符

Archon在验证过程中，发现了原始证明计划里藏着一个逻辑漏洞。它拒绝了原方案，重新设计了技术路线，然后继续。这不是“AI按指令执行”，而是更接近人类数学家的工作方式：发现错误，承认错误，推倒重来。

#但仅仅“找到答案”还不够

数学和其他学科有一个根本区别：

你必须证明你是对的。

不是大概对，不是实验符合预期，是铁板钉钉、无懈可击的逻辑推导。

这时候另一个AI智能体上场了。

它的工作：把Rethlas这个智能体给的自然语言证明，转化成Lean 4形式化代码，也就是可以让计算机逐行验证、不允许任何模糊的数学语言。

最后用80个小时产出了19,000行代码，42个文件。

数学界有个参照：经验丰富的形式化专家，每天能写150到250行Lean代码。

按这个速度，19,000行——几个专家几个月。

北大团队的AI：80小时。

为什么用Lean 4？

人类写数学证明，会有一些"偷懒"的地方

比如数学家写证明时会写：

"显然可得..."

"由已知条件，显然有..."

"这一步同理可得..."

这些显然，其实藏着很多没说清楚的逻辑跳跃。

比如1+1=2。如果数学家每次都要写这样的推导，他们早就疯了！但其实只要某一步的显然藏着微小的逻辑漏洞，那整篇论文推导就全错了！

而轮到同行评审的时候，审稿人有时候会放过，有时候会问一句"这里怎么来的"，有时候自己也没注意就过了。

但是Lean 4不允许"显然"

Lean 4会逐行检查：

每一步推导，必须有明确的前因后果，不能跳步，不能用直觉代替逻辑，不能说"显然"，必须写出每一步的严格理由。就是为了堵人类的嘴！

国内首次

这是国内首次，AI全流程自动发现并验证数学猜想。

不依赖DeepMind，不依赖OpenAI的数学工具。

北大团队自研了框架，开源了代码。

但团队自己也承认：底层的语言模型，目前仍依赖国外模型。

他们没有藏着掖着。

成果是真实的，局限也是真实的。

这件事真正厉害的地方

不是“AI比数学家聪明了”。

数学家很聪明。但每个数学家只有一个大脑，只有一段时间，只在一个领域里深挖。

研究“局部环”特定性质的学者，很难跨越数十年的文献库去读整环完备化的老论文。这不是懒，是物理上不可能——人类大脑的带宽是有限的。

AI没有这个约束。

它什么都看过，没有遗忘曲线，没有阅读盲区。然后它把两件事连在了一起：一件发生在2014年，一件发生在2006年。

连接的那一刻，答案就有了。

这才是AI在数学里最可怕的能力——不是算得快，是它什么都看过。

这只是一个开始。

过去几千年，人类文明的进步，建立在一种极其低效的传承上：老一辈学者把知识压缩成直觉，写进书里；新一辈学者花几十年解压，然后再试图往前走半步。

这种基于“肉体大脑”的接力赛，因为带宽的限制，已经快到物理极限了。

Anderson 猜想之所以搁置 12 年，就是因为没有人的大脑，能同时装下交换代数和 20 年前所有的冷门领域。

而北大 AI 团队这次的突破，告诉我们：

未来的科学前沿，可能不再属于那些试图在大脑里装下整个图书馆的“通才”，而是属于那些知道“如何向 AI 描绘蓝图”的架构师。

参考来源：

• 北大FrenzyMath团队技术报告（2026年4月4日）: https://frenzymath.com/blog/conjecture/
• Haocheng Ju et al. (2026) "Automated Conjecture Resolution with Formal Verification", arXiv:2604.03789
• China Research Collective报道: https://chinaresearchcollective.substack.com/p/a-new-breakthrough-in-ai-solving
• 开源代码仓库: https://github.com/frenzymath/Rethlas