AI 系统在 Lean4 中形式化生成并验证 Erdős 问题 #124 的证明，标志着自动化定理证明（ATP）进入新阶段。该问题由 Burr、Erdős、Graham 和 Li 提出：给定整数序列 (3 \leq d_1 < d_2 < \cdots < d_k) 满足 (\sum_{i=1}^k \frac{1}{d_i - 1} \geq 1)，是否存在足够大的整数皆可表示为 (\sum c_i a_i)，其中 (c_i \in {0,1})，(a_i) 在基 (d_i) 下仅含 0 和 1 数字？Pomerance 证明该条件必要性，原作证明了 ({3,4,7}) 情况成立。
DeepMind 等团队已将该猜想形式化为 Lean4 代码（github.com/google-deepmind/formal-conjectures），Hacker News 热议“AI just proved Erdos Problem #124”。本文聚焦单一技术点：提示工程驱动的 Lean4 验证管道，结合 Erdos #707 先例（GPT-5 生成 6000 行代码，含 26 定义、169 引理、4 定理，验证 <30s），提供可落地参数与清单。
观点：提示工程是 ATP 核心，迭代反馈优于零样本
传统 ATP 如 LeanDojo 依赖监督数据，而提示工程通过“vibe coding”（人类-AI 交互）生成复杂证明。Erdos #124 形式化需分解为：(1) 翻译自然语言为 Lean 语句；(2) 导入 mathlib；(3) tactic 搜索证明路径。证据：DeepMind repo 显示 Lean 代码精确捕捉 sum 条件与表示形式；类似 #707，GPT-5 经一周迭代（人类反馈修正 hallucination）输出可编译证明。
优势：减少数据依赖，适应新问题。DeepSeek-Prover 等模型在 MiniF2F 达 70%+ 成功率，证明迭代提示有效。
证据：Lean4 管道实证
Lean4 编译器提供精确反馈（类型错误、未闭合目标），远超 LLM 内在不确定性。#707 案例：26 定义 + 169 引理，笔记本验证 <30s。#124 形式化类似，利用 Mathlib.Combinatorics 等库。
关键步骤：
-
语句形式化：Prompt “将以下猜想翻译为 Lean4 theorem，使用 Mathlib： [问题描述]”。输出如：
theorem erdos_124 (d : ℕ → ℕ) (hd : ∀ i, 3 ≤ d i) (hsum : ∑ i in Finset.range k, 1 / (d i - 1) ≥ 1) : ∃ N, ∀ n ≥ N, ∃ c : Fin k → Bool, n = ∑ i, if c i then a_i else 0 ∧ ∀ i, a_i.digits (d i).toNat ⊆ ({0,1}) ...
迭代 3-5 次修正类型。
-
证明生成：Prompt “使用 tactic 模式证明上述 theorem，优先 rw、simp、ring 等”。分 lemma 构建：先证必要性，再充分大 N。
-
验证：lake verify 检查，超时阈值 60s/文件。
实证：#707 证明通过普通 PC 验证，零错误。
可落地参数与清单
提示模板清单（复制即用）：
- 分解提示： “Step 1: 定义 Sidon-like 结构。Step 2: 证明 sum 条件蕴涵表示。使用 exact、simp。”
- 反馈循环： “上步错误：[Lean 报错]。修正 tactic。”
- 搜索提示： “探索 5 条路径，使用 aesop 或 eblast，预算 2048 tokens。”
管道参数：
| 参数 |
值 |
理由 |
| Max iterations |
10 |
防循环，#707 用 7 次收敛 |
| Timeout/step |
30s |
平衡速度，笔记本友好 |
| Lemma granularity |
5-20/证明 |
易生成，mathlib 重用率高 |
| Model |
GPT-5 / DeepSeek-Prover |
数学专用，pass@1 >70% |
| Retry on fail |
3x |
随机性补偿 |
监控点：
- 编译率：目标 >95%，低于 80% 换 prompt。
- Proof length：<5000 行，超长拆分。
- Coverage：mathlib 依赖 <50%，防黑箱。
部署清单：
- 安装 Lean4 + lake。
- VSCode + Lean4 extension。
- Git clone DeepMind repo，lake build。
- 脚本：
while ! lake verify; do gpt-prompt-fix; done。
- 回滚：手动 lemma，若 3 迭代失败，转人类。
风险：(1) Hallucinated lemma，限：Lean 即验；(2) 搜索爆炸，限：预算 2048×2×600 tactics。回滚：fallback 到 LeanDojo SFT 模型。
此管道适用于任意 Erdos 问题，扩展至 PFR 等。未来，Lean-GPT 插件将无缝集成。
资料来源：
- erdosproblems.com/124
- HN: news.ycombinator.com/item?id=419... (AI proved #124)
- DeepMind: github.com/google-deepmind/formal-conjectures/124.lean
- #707 论文: borisalexeev.com/pdf/erdos707.pdf（类似实践）