### [Claude真把概率论“圣杯”推倒了？9.7万行Lean代码通过双内核检查，但人类同行评审还没开始](https://www.zuoshipin.com/article/48323)

**Published:** 2026-10-08T12:38:20

**Author:** 天才交易员

**Excerpt:** Anthropic开源formal-math渗流项目，Claude生成约9.7万行Lean代码，证明θ(pc)…

**形式化证明已经过机械验证，数学命题与证明价值仍需独立专家确认。**

**导读：**GitHub上出现了一套由Claude生成的Lean证明工程，目标直指概率论与统计物理中长期开放的渗流猜想：所有d≥2维最近邻伯努利键渗流，在临界概率pc处都没有无限开放簇。代码通过了Lean内核和独立nanoda内核重放，仓库也公开了完整审计。**但“机器检查通过”与“数学界已经正式接受”之间，仍隔着命题忠实度审阅和独立人类同行评审。**

[![Anthropic formal-math渗流证明项目的核心命题](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-cover.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-cover.webp)

Anthropic formal-math渗流证明项目的核心命题

## 先把结论说准：Claude证明的到底是什么？

项目的形式命题是：对超立方格ℤd上的最近邻伯努利**键渗流**，当d≥2时，临界点pc处原点的开放簇几乎必然有限，即θ(pc)=0。

这覆盖了此前长期开放的3至10维情形。二维结果来自Harris与Kesten；11维及以上已有lace expansion等方法。仓库同时谨慎注明：它形式化的是θ(pc)=0，经典理论可由此得到连续性结论，但“θ在整个\[0,1\]上连续”本身不是Lean里的正式主命题。

[![formal-math仓库对渗流证明范围与审查状态的说明](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image03.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image03.webp)

formal-math仓库对渗流证明范围与审查状态的说明

**准确状态：**Lean工程能完整构建，关键命题经过comparator与独立nanoda内核重放；仓库同时明确写着，尚未由作者之外的人类数学家独立同行评审。现阶段应称为“高度可验证的公开形式化证明成果”，不宜直接写成数学共同体已经最终盖章。

## 为什么它被叫作概率论“圣杯”？

渗流模型可以想成一张无限网格，每条边以概率p开放。p很小时，开放边只形成零散小簇；p足够大时，会出现延伸到无穷远的巨大连通簇。两种状态切换的分界线就是临界概率pc。

[![渗流理论早期研究者Simon与Hammersley](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image07.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image07.webp)

渗流理论早期研究者Simon与Hammersley

[![不同开放概率下的伯努利键渗流示意](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image08.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image08.webp)

不同开放概率下的伯努利键渗流示意

问题在于：恰好站在临界点时，会不会已经出现无限簇？二维有平面几何与对偶工具，高维可利用均场行为，而3至10维既缺二维特殊结构，也没有足够强的高维近似，因此卡了几十年。

[![渗流临界概率与无限连通簇问题](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image04.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image04.webp)

渗流临界概率与无限连通簇问题

[![二维方格渗流临界点的直观说明](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image09.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image09.webp)

二维方格渗流临界点的直观说明

[![二维渗流中θ(pc)=0的经典结果](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image10.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image10.webp)

二维渗流中θ(pc)=0的经典结果

[![Kesten关于二维键渗流临界概率的经典论文](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image12.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image12.webp)

Kesten关于二维键渗流临界概率的经典论文

## 菲尔兹奖得主刚写“只剩时间问题”，仓库已经放出证明

2022年菲尔兹奖得主Hugo Duminil-Copin长期研究渗流与相变。他在2026年8月30日发表文章时仍写道，θ(pc)=0很可能在数学家之前被前沿模型证明，并讨论这种变化对数学文化、青年训练与研究过程的冲击。

[![Hugo Duminil-Copin讨论AI与渗流公开猜想](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image01.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image01.webp)

Hugo Duminil-Copin讨论AI与渗流公开猜想

[![菲尔兹奖得主Hugo Duminil-Copin](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image11.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image11.webp)

菲尔兹奖得主Hugo Duminil-Copin

[![Hugo Duminil-Copin在统计物理领域的研究分享](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image13.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image13.webp)

Hugo Duminil-Copin在统计物理领域的研究分享

[![Hugo Duminil-Copin讲解渗流与相变问题](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image14.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image14.webp)

Hugo Duminil-Copin讲解渗流与相变问题

需要纠正一个流量化说法：**“AI跨过菲尔兹奖终点线”不是正式奖项判断。**有数学家认为这类成果若由人类完成会是顶级成就，但菲尔兹奖评选看的是长期、综合贡献，也不会因为一个仓库通过编译就自动产生获奖结论。

[![关于AI攻克概率论难题的讨论摘录](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image02.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image02.webp)

关于AI攻克概率论难题的讨论摘录

[![AI解决概率论圣杯问题的报道标题](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image06.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image06.webp)

AI解决概率论圣杯问题的报道标题

## 真正的突破口：不是蛮力，而是接住了Kozma–Nitzan的归约

2024年，Gady Kozma与Shahaf Nitzan把θ(pc)=0问题归约到有限加权图上的一组“gluing inequalities”。他们证明，只要其中最弱的Conjecture 3成立，就能推出所有d≥2维上的目标结论。

[![Kozma与Nitzan将θ(pc)=0归约到猜想不等式的论文](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image16.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image16.webp)

Kozma与Nitzan将θ(pc)=0归约到猜想不等式的论文

[![3至10维渗流问题长期未解的说明](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image17.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image17.webp)

3至10维渗流问题长期未解的说明

[![Kozma与Nitzan提出的关键连接不等式](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image18.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image18.webp)

Kozma与Nitzan提出的关键连接不等式

Anthropic项目走的正是这条路线。仓库声称先证明一个更强的**additive gluing inequality**，再推出Kozma–Nitzan Conjecture 3，并在Lean中重新形式化归约链所需要的经典结果。

核心新工具被称为**conditioned slack hierarchy**：它把一族条件协方差不等式按辅助顶点列表分层，通过归纳把局部关系传递成可用于gluing的全局界。它不是让模型穷举全部图形，而是寻找并编码一条新的数学结构。

## 9.7万行代码如何证明自己“没有偷偷跳步”？

仓库的审计信息给出了多层检查：

-   **固定工具链：**Lean 4 v4.32.0与指定Mathlib提交，避免依赖漂移。
-   **完整构建：**记录显示约251个Lean文件、97574行代码可完整通过构建。
-   **sorry检查：**证明库与Solution中没有sorry；Challenge文件保留的两个sorry是刻意放置的待证命题占位。
-   **公理检查：**主定理只依赖propext、Classical.choice与Quot.sound，没有额外新增公理。
-   **独立内核：**comparator把Solution与可信命题文件比较，并用nanoda内核重放关键证明。

[![数学界对θ(pc)=0形式化证明的公开讨论](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image05.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image05.webp)

数学界对θ(pc)=0形式化证明的公开讨论

[![关于AI生成形式化证明与人类审查的讨论](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image15.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image15.webp)

关于AI生成形式化证明与人类审查的讨论

## 机械证明通过，为什么还不能省掉人类审阅？

| 验证层 | 能确认什么 | 仍不能确认什么 |
| --- | --- | --- |
| **Lean内核** | 每一步类型检查成立，没有未证明跳步 | 定义是否忠实表达原始数学问题 |
| **独立内核重放** | 降低单一实现或工具链错误风险 | 证明是否提供人类可理解的新思想 |
| **人类同行评审** | 检查命题忠实度、引用、范围与数学意义 | 无法替代内核对数万行细节的逐步验证 |

[![研究者讨论Anthropic形式化证明的影响](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image19.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image19.webp)

研究者讨论Anthropic形式化证明的影响

[![数学家尝试审阅并泛化Claude生成的Lean证明](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image20.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image20.webp)

数学家尝试审阅并泛化Claude生成的Lean证明

[![原作者对独立验证和人类可读证明保持谨慎](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image21.webp)](https://admin.zuoshipin.com/wp-content/uploads/2026/10/claude-percolation-lean-image21.webp)

原作者对独立验证和人类可读证明保持谨慎

因此，这不是“AI证明不可信”，也不是“Lean通过就无需审稿”。更合理的结论是：**机器已经把局部逻辑正确性推到前所未有的强度，人类审阅则转向定义、范围、解释和学术价值。**

## 复现教程：自己验证仓库，而不是只看新闻标题

项目说明建议准备约13GB磁盘与32GB内存。工具链和依赖均固定到具体版本，不应随意运行更新命令。

1.  安装Git与elan，让项目自动选择固定Lean版本。
2.  克隆Anthropic formal-math仓库，进入percolation目录。
3.  下载Mathlib缓存并执行完整构建。
4.  运行Axioms脚本，检查主定理依赖。
5.  进一步按AUDIT.md运行comparator检查。

```
git clone https://github.com/anthropics/formal-math.git
cd formal-math/percolation
lake exe cache get
lake build
lake env lean scripts/Axioms.lean
```

构建成功只代表你复现了仓库记录。真正的数学审阅还要打开Challenge.lean，逐个核对zdGraph、bondPercolation、theta、criticalProb与PercolationContinuity是否准确对应教材定义。

## 做视频网观点

这次最值得记住的不是“Claude抢走菲尔兹奖”，而是**AI第一次把发现、形式化、编译反馈和审计流程连成了一条公开、可复现的数学生产线**。它没有让数学家失去作用，而是把最稀缺的工作从逐行推导推向选题、建模、定义审阅与解释。

如果独立审阅最终确认形式化命题完全忠实，这会是一项非常重要的AI数学成果；如果审阅发现定义或归约边界有偏差，公开仓库同样让问题可以被迅速定位。两种结果都比只凭一段自然语言“相信模型证明了”更成熟。

## 相关站内内容

**Anthropic Formal Math站内导航：**[https://www.zuoshipin.com/link/48322.html](https://www.zuoshipin.com/link/48322.html)

**Claude站内导航：**[https://www.zuoshipin.com/link/876.html](https://www.zuoshipin.com/link/876.html)

**PrimeGaps186形式化数学项目：**[https://www.zuoshipin.com/link/32209.html](https://www.zuoshipin.com/link/32209.html)

**GPT-6 Astra数学研究解析：**[https://www.zuoshipin.com/article/32210](https://www.zuoshipin.com/article/32210)

**Claude中文界面与地区限制：**[https://www.zuoshipin.com/article/47630](https://www.zuoshipin.com/article/47630)

## 官方与一手资料

[Anthropic Formal Math渗流项目](https://github.com/anthropics/formal-math/tree/main/percolation)

[项目机械验证与审计记录](https://github.com/anthropics/formal-math/blob/main/percolation/AUDIT.md)

[Kozma–Nitzan：将θ(pc)=0归约到猜想不等式](https://arxiv.org/abs/2401.12397)

[Hugo Duminil-Copin：AI与数学研究过程的反思](https://proofsandprompts.com/2026/08/30/care-for-a-little-more-ai/)

**Tags:** Anthropic, Claude数学, Lean 4, 形式化数学, 渗流理论

**Categories:** AI资讯

---