用 Codex 和 Claude 智能体将 OpenAI 数学证明的 Lean 代码缩减 24.65%
Show HN: Reducing an OpenAI proof by 25% in a few hours
一项实验用 Codex 和 Claude 智能体把 OpenAI 的 Unique Games 证明从 151,287 行 Lean 代码缩减到 113,990 行，减少 24.65%，定理陈述保持不变。过程由多轮智能体反复修改与校验完成，最终证明通过 Lean 内核检查，仅使用 propext、Classical.choice 和 Quot.sound 三条公理，未使用 sorryAx。
OpenAI 公布了一组证明，许多人正试图解读这对他们所在领域整体意味着什么。
这里的目标是为讨论补充一个数据点。
151,287 → 113,990 行 Lean 代码：减少了 24.65%。 空行和注释不计入。定理陈述保持不变。
这个实验探究 AI 模型能将现有证明压缩多少。过程很简单：做出修改、检查修改、保存可用的版本，然后重复。起点是来自 openai/math 的 Unique Games 证明。
这是一个耗时几小时的副项目。几个提示词搭建起循环，随后智能体们反复进行多轮修改和检查。
进展
每一行都使用相同的计数方法。它统计证明及其所需的本地文件。
| 阶段 | 模型与设置 | 剩余行数 |
|---|---|---|
| 原始 | 原始证明 | 151,287 |
| 第 18–19 轮 | Codex 智能体，一个接一个 | 141,443 |
| 第 20 轮 | 一个 Claude 智能体 | 120,980 |
| 第 21 轮 | 四个 Codex 智能体同时工作 | 120,571 |
| 第 22 轮 | 24 个 Codex 智能体，每个都有独立的工作副本 | 117,213 |
| 第 23 轮 | 另一组 24 个 Codex 智能体 | 113,990 |
Pi 报告的模型名称：
- 第 18–19 轮和第 21 轮：
openai-codex/gpt-6.1-sol - 第 20 轮：
claude-agent/claude-fable-5-1 - 第 22–23 轮：
openai-codex/gpt-6-astra
全部使用高思考设置。更早的尝试没有产生被保留的修改。提示词要求减少 10% 或 40%，但这些是目标，而非每一轮的结果。
智能体们删除了重复代码并复用了现有证明。在后续轮次中，它们共享构建结果，但各自的工作文件保持独立。最多可同时运行四条构建命令。每组完成后，它们的修改会被合并并一起检查。
检查
- 两个版本都从空的项目构建文件夹成功构建。外部库的现有构建被复用。
- 最终定理陈述与原始版本一致。Lean 的内核（用于检查证明）再次检查了最终证明并予以接受。
- 该证明仅使用允许的公理：
propext、Classical.choice和Quot.sound。它不使用sorryAx，后者允许未完成的证明。 - 受保护的模型和测试文件、Lean 4.34.1 以及外部库的版本均保持不变。额外的 Nanoda 检查未运行。
- 所有新增的辅助代码都被计入。从原始仓库中移除无关项目不算作减少。
核对数字
Git 历史从 original-minimal 开始，随后是 simplified。最终计数包含所有项目证明文件，甚至包括不再使用的文件。
python3 scripts/audit_proof.py --before-repo . --before-rev original-minimal \ --after-repo . --after-rev simplified --output /tmp/wiggums-audit
参见如何重复检查并阅读结果。
许可证：Apache-2.0。参见源代码和变更详情。 本 README 由主导这项工作的 AI 应 Roelof 的要求撰写。
来源：Hacker News · github.com