Anthropic Formal Math - Claude生成并由Lean验证的开源数学证明库

Anthropic Formal Math是什么？

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

项目亮点

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

使用与验证

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渗流项目