形式化证明已经过机械验证，数学命题与证明价值仍需独立专家确认。
导读：GitHub上出现了一套由Claude生成的Lean证明工程，目标直指概率论与统计物理中长期开放的渗流猜想：所有d≥2维最近邻伯努利键渗流，在临界概率pc处都没有无限开放簇。代码通过了Lean内核和独立nanoda内核重放，仓库也公开了完整审计。但“机器检查通过”与“数学界已经正式接受”之间，仍隔着命题忠实度审阅和独立人类同行评审。
先把结论说准：Claude证明的到底是什么？
项目的形式命题是：对超立方格ℤd上的最近邻伯努利键渗流，当d≥2时，临界点pc处原点的开放簇几乎必然有限，即θ(pc)=0。
这覆盖了此前长期开放的3至10维情形。二维结果来自Harris与Kesten；11维及以上已有lace expansion等方法。仓库同时谨慎注明：它形式化的是θ(pc)=0，经典理论可由此得到连续性结论，但“θ在整个[0,1]上连续”本身不是Lean里的正式主命题。
准确状态：Lean工程能完整构建，关键命题经过comparator与独立nanoda内核重放；仓库同时明确写着，尚未由作者之外的人类数学家独立同行评审。现阶段应称为“高度可验证的公开形式化证明成果”，不宜直接写成数学共同体已经最终盖章。
为什么它被叫作概率论“圣杯”？
渗流模型可以想成一张无限网格，每条边以概率p开放。p很小时，开放边只形成零散小簇；p足够大时，会出现延伸到无穷远的巨大连通簇。两种状态切换的分界线就是临界概率pc。
问题在于：恰好站在临界点时，会不会已经出现无限簇？二维有平面几何与对偶工具，高维可利用均场行为，而3至10维既缺二维特殊结构，也没有足够强的高维近似，因此卡了几十年。
菲尔兹奖得主刚写“只剩时间问题”，仓库已经放出证明
2022年菲尔兹奖得主Hugo Duminil-Copin长期研究渗流与相变。他在2026年8月30日发表文章时仍写道，θ(pc)=0很可能在数学家之前被前沿模型证明，并讨论这种变化对数学文化、青年训练与研究过程的冲击。
需要纠正一个流量化说法：“AI跨过菲尔兹奖终点线”不是正式奖项判断。有数学家认为这类成果若由人类完成会是顶级成就，但菲尔兹奖评选看的是长期、综合贡献，也不会因为一个仓库通过编译就自动产生获奖结论。
真正的突破口：不是蛮力，而是接住了Kozma–Nitzan的归约
2024年，Gady Kozma与Shahaf Nitzan把θ(pc)=0问题归约到有限加权图上的一组“gluing inequalities”。他们证明，只要其中最弱的Conjecture 3成立，就能推出所有d≥2维上的目标结论。
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内核重放关键证明。
机械证明通过，为什么还不能省掉人类审阅？
| 验证层 | 能确认什么 | 仍不能确认什么 |
|---|---|---|
| Lean内核 | 每一步类型检查成立，没有未证明跳步 | 定义是否忠实表达原始数学问题 |
| 独立内核重放 | 降低单一实现或工具链错误风险 | 证明是否提供人类可理解的新思想 |
| 人类同行评审 | 检查命题忠实度、引用、范围与数学意义 | 无法替代内核对数万行细节的逐步验证 |
因此，这不是“AI证明不可信”，也不是“Lean通过就无需审稿”。更合理的结论是：机器已经把局部逻辑正确性推到前所未有的强度，人类审阅则转向定义、范围、解释和学术价值。
复现教程：自己验证仓库，而不是只看新闻标题
项目说明建议准备约13GB磁盘与32GB内存。工具链和依赖均固定到具体版本，不应随意运行更新命令。
- 安装Git与elan，让项目自动选择固定Lean版本。
- 克隆Anthropic formal-math仓库，进入percolation目录。
- 下载Mathlib缓存并执行完整构建。
- 运行Axioms脚本，检查主定理依赖。
- 进一步按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
Claude站内导航：https://www.zuoshipin.com/link/876.html
PrimeGaps186形式化数学项目：https://www.zuoshipin.com/link/32209.html
GPT-6 Astra数学研究解析：https://www.zuoshipin.com/article/32210
Claude中文界面与地区限制：https://www.zuoshipin.com/article/47630
