### [Anthropic Formal Math – Claude生成并由Lean验证的开源数学证明库](https://www.zuoshipin.com/link/48322.html)

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

**Author:** 天才交易员

**Excerpt:** Anthropic Formal Math公开Claude生成的Lean形式化数学证明，包含渗流θ(pc)=0…

## Anthropic Formal Math是什么？

**Anthropic Formal Math是一个公开AI生成形式化数学证明的GitHub项目库。**其中percolation子项目使用Lean 4与Mathlib，形式化证明伯努利键渗流在临界点满足θ(pc)=0，并覆盖此前长期未解决的3至10维情形。

[![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渗流证明项目的核心命题

## 项目亮点

-   **AI生成：**仓库说明Lean代码由Claude模型在负责人指导下自主生成。
-   **机械检查：**固定Lean与Mathlib版本，可通过Lean内核重新构建。
-   **独立内核重放：**关键命题还使用comparator与nanoda内核复核。
-   **审计公开：**AUDIT.md记录工具链、构建结果、sorry与额外公理检查。
-   **可读说明：**提供15页证明导读，但项目强调它不是正确性的最终凭据。

[![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仓库对渗流证明范围与审查状态的说明

## 使用与验证

1.  准备Git、elan、Lean工具链与足够磁盘空间。
2.  克隆formal-math仓库并进入percolation目录。
3.  运行依赖缓存命令，再执行完整构建。
4.  运行Axioms脚本检查主定理依赖的公理。
5.  按AUDIT.md运行comparator，核对可信命题文件与证明实现。

```
lake exe cache get
lake build
lake env lean scripts/Axioms.lean
```

## 重要边界

项目已经通过机械检查，但仓库明确说明尚未经过独立人类同行评审。Lean内核检查的是“代码是否证明了代码中的命题”，数学家还需要审阅定义、形式化忠实度、引用链与人类可读解释。

## 官方入口

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



---