Claude 攻克渗流理论难题：生成 Lean 证明代码，破解数十年数学猜想

前脚刚有菲尔兹奖得主感叹「AI 迟早会像推土机一样推平我们领域最著名的猜想」，后脚大模型就真的把这道难关给推平了。

Anthropic 旗下的大语言模型 Claude 在研究人员的指导下，成功给出了概率论渗流理论核心猜想的完整证明，甚至直接写出了可以通过形式化验证语言 Lean 严格检验的代码。没有开新闻发布会，也没有官方博客大肆宣扬，数学界却直接被震动了。

困扰数学界数十年的「管道网络」

渗流理论最早可以追溯到 1957 年，当时研究者想搞明白液体是怎样渗过海绵这种多孔材料的。数学家把这抽象成由管道连成的庞大网络，每根管道都有一定概率处于开启或闭合状态。

当开启概率低于某个临界阈值时，管道连不成大气候；一旦超过临界值，整个网络就可能出现无限大的连通区域。这个临界转变到底长什么样，一直是概率论皇冠上的明珠。

德国布伦瑞克工业大学数学家 Benedikt Jahnel 曾评价，谁要是搞定这个问题，大概率能拿菲尔兹奖。2022 年凭借相变研究斩获菲尔兹奖的法国数学家 Hugo Duminil-Copin 也曾试图攻克它，却同样铩羽而归。

补齐 3 到 10 维的关键拼图

数学界此前已经证明，在 1 维和 2 维网络中，这种相变是连续发生的，几率不会突然从零跳跃到一个固定数值；而在 11 维及以上的超高维空间里，借助统计平均性质，人类也早就证明了它是连续的。

真正卡住所有顶尖学者的盲区，偏偏是夹在中间的 3 到 10 维。这也是人类现实世界最关心的几类空间维度。

2026 年 8 月 30 日，Hugo Duminil-Copin 还在博客上写道，AI 攻破该领域最著名的猜想只是时间问题。没想到仅仅几天后，Anthropic 就放出了证明结果，Claude 证明了 3 到 10 维网络下的相变同样是连续的。

更关键的是，它不仅给出了自然语言的论证逻辑，还附带了经 Lean 编译器逐行验证通过的代码，彻底堵死了大模型常见的逻辑幻觉漏洞。Jahnel 坦言自己的心情很复杂，既为猜想终于被证实感到高兴，又对最后这关键一步竟然由 AI 完成感到某种失落。

为什么重要

对从事纯数学和理论物理的研究者来说，这件事标志着 AI 的定位变了。过去大模型在数学领域的亮点多半停留在国际奥赛做题，现在它证明了自己能在人类顶尖学者的引导下，啃下数十年没人解开的真正猜想。

我们认为，Anthropic 这次最聪明的做法，是把大模型的生成能力与形式化验证语言 Lean 绑在了一起。数学家最怕大模型一本正经地胡说八道，而 Lean 就像一个不讲情面的机器判官，能编译通过就代表逻辑绝对无懈可击，一举消除了对 AI 幻觉的疑虑。

但这也暴露了当前的局限：Claude 依然是在人类研究者的持续提示与框架拆解下完成证明的，还谈不上独立发现数学定理。它更像是一台算力和逻辑推演能力极度强大的推土机，方向盘暂时还握在人类手里。

这一步迈出后，同行竞争的压力立刻来到了 OpenAI 和 Google DeepMind 这边。未来的数学研究竞争，可能不再单拼人类数学家的大脑，而是拼谁能更早把顶级学者与形式化验证 AI 深度绑定，纯数学研究的产出节奏很可能会被彻底改写。