Claude在GitHub提交了一个仓库，菲尔兹奖得主说"这只是一个时间问题"
2026年8月30日，概率论大师、菲尔兹奖得主Hugo Duminil-Copin写了一篇带着点忧伤的博客。他提到，在概率论领域，最著名的那个猜想倒在AI的推土机下，恐怕只是个时间问题。
几乎同时，有人发现Anthropic工程师Justin Leder提交了一个代码仓库。没有发布会，没有官方公告，仓库里躺着的是一份由Claude自动生成、并用Lean形式化证明语言严格验证的完整证明——渗流理论中的连续相变猜想，被AI证明了。
这道题困扰了人类近70年。
1957年，数学家Simon Broadbent和John Hammersley提出了一个关于液体穿透多孔介质的猜想。在数学上，它被抽象为一个网格模型：每条边以概率p连通，当p达到某个临界值时，系统会发生相变——从局部连通突变为无限连通。问题是，在恰好等于临界概率的那一刻，是否已经存在无限连通分量？
这个问题被称为θ=0猜想，是概率论中的"圣杯"。
二维情况下，1980年Harry Kesten解决了它。超高维度（11维以上），数学家也用均场论等工具证明了。但3到10维——这个区间既没有二维的对称性红利，又够不到高维的统计平滑，成了几十年间无数数学家撞上的叹息之墙。
真正的转折发生在2024年。以色列魏茨曼科学研究所的Gady Kozma和佐治亚理工学院的Shahaf Nitzan发表了一篇论文，证明了一个关键思路：如果某个特定的代数不等式成立，那么3到10维的θ=0猜想就自动成立。
问题从"证明一个几何猜想"压缩成了"证明一个不等式"。
但这个不等式像一条滑溜的泥鳅。数学家们尝试构建辅助函数、寻找上下界，总在推导的关键节点遭遇奇异性崩溃。Kozma本人对此保持沉默，他在采访中说："我们还在等待Anthropic发布一个人类能看懂的版本，并解释他们到底是怎么做到的。"
Anthropic的回应很直接：代码已经开源在GitHub上，Lean形式化验证已经通过。
德国布伦瑞克工业大学数学家Benedikt Jahnel说，如果有人类证明了这个猜想，他大概率能拿菲尔兹奖。"但现在，是AI跨过了终点线。"
Gil Kalai的反应更克制："如果得到验证，这将是一项非凡的突破。"
宾夕法尼亚大学的Ahmed Bou-Rabee用一天时间对证明进行了泛化和修改。他的评价带着某种复杂的羡慕："AI让我做到了我以前连想都不敢想的事。有些研究项目我苦苦做了整整八年，几乎毫无进展，但在AI的协助下，我现在距离彻底解决只有一步之遥。"
这不是Claude第一次展示形式化证明能力。但这次的特殊之处在于，它解决的是一道人类顶级数学家多年未能攻克的开放问题，而不是一个教学或竞赛级别的练习。
Duminil-Copin在博客中写道，解开一个数学问题，过程往往比结果更重要。他自己的菲尔兹奖工作，正是在攻克渗流猜想失败后结出的"副产物"。"那些失败的尝试催生了几十个全新的想法，我把它们用在其他领域，带来了许多我从未想象过的重大发现。"
AI的推土机不体会迷茫，也不懂得审美。它只是用严密的符号逻辑，把那条泥鳅摁死了。
数学史从来不只是关于定理的编年史。费马大定理的证明催生了代数几何的壮丽宏图，黎曼猜想的追寻拔地而起了解析数论的大厦。证明本身可能由机器完成，但接下来会发生什么——人类数学家会如何消化这些机器带回来的智慧碎片，会衍生出什么新的工具和视角——这才是真正值得盯着看的事情。
GitHub上的仓库链接在那里：https://github.com/anthropics/formal-math/tree/795efb86f191735c5481675763537cfb4ff37e55/percolation
证明是否完整、Lean验证是否经得起同行审视、人类数学家如何从中提取新的洞察——这些问题都还在路上。但有一点已经清楚：那道困扰人类半个多世纪的门槛，AI已经跨过去了。