《当代码学会证定理：一次三百块，两题等了五十六年》 —— AlphaProof Nexus 深度解读

1996年，Paul Erdős 提出了一个问题。这位数学界的吉普赛人，一生提出了超过1500个开放问题——他管数学里任何一个难啃的骨头叫"值得付钱的"。有的问题值25美元，有的值1000。他没来得及为 #125 定价。这个问题活了30年，没人解开。

2026年春天，一台机器在几个小时内证完了。花费：不到300美元。

问题是这样的：A 是所有用 0 和 1 写出来的三进制数的集合（比如 10、101、1101）。B 是所有用 0 和 1 写出来的四进制数的集合。把 A 和 B 加起来——A+B，所有可能的两两之和——这个集合够不够"稠密"？直说便是：取到足够大的 N，A+B 里小于 N 的元素个数除以 N，能不能始终大于某个正数？

三段话，讲清了一个悬了30年的问题。机器给的答案，你可能猜到了——不能。稠密度为零。证法极巧：利用 \(3^m \approx 4^k\) 的丢番图逼近，构造了一个归纳式"削薄"论证，一层一层地把不可能的元素剔除干净。

这非孤例。同一台机器在同一天里，还解了另外8个 Erdős 问题。

🧮 一架分不清真假的推理引擎

先说这件事为什么难。

LLM 做数学推理，有一个致命缺陷：你不知道它哪句对、哪句错。 让它证一个定理，它可能写出十个步骤，前九步都对，第十步凭空编了一个引理——那个引理恰好是错的。但论证读起来滴水不漏。

数学界对这种事极度严肃。一篇文章发出去，审稿人花几个月逐行检查。一个大定理可能有多位数学家交叉验证。非迷信——实为经验告诉他们，人脑做长链推理，就是会出错。LLM 出错的频率和方式，比人脑更难预测。

那能不能不让人来检查？

能。用编译器。

Lean 是一种形式化证明语言。在 Lean 里写证明，等于写一段程序。Lean 的编译器逐行验证，少一个逻辑步骤就报错。编译通过 = 证明正确。没有中间地带。

AlphaProof Nexus——Google DeepMind 的这套系统——做了一件事：把 LLM 放进一个 Lean 编译器的笼子里，让它生成证明草案，编译器当场验证，错了打回重写，对了才算数。

你也可以这么理解：LLM 负责"想"，Lean 负责"判"。想错了就重想。想对了就通过。两者交替，直到证完为止。

🏗️ 两种智能体，一条铁律

AlphaProof Nexus 里住了两种智能体。

基础版（Agent A）：极简。把问题丢给 Gemini 3.1 Pro，模型生成证明草案，Lean 编译。报错了，模型看报错信息，改，再编译。循环。N 个独立的"证明子智能体"同时跑，谁先跑通谁赢。

完整版（Agent D）：在基础版之上叠了三个模块。

一是 AlphaProof——DeepMind 此前为数学奥林匹克开发的形式化证明引擎。子智能体在证到中途卡住时，可以把某个子目标扔给 AlphaProof："这个帮我证一下"。AlphaProof 返回三样之一：证明成功、证伪了（这个子目标不成立）、搞不定。

二是进化搜索。把每一轮生成的证明草图（编译通过但尚有 sorry 残留的"半成品"）存进一个种群数据库。用 Gemini 3.0 Flash 做同行评议——批量抽取7个草图，按清晰度、可行性和数学新颖度排个序。排名高的获得更高的 Elo 分，下一轮被抽中"繁殖"的概率更大。

三是全局目标缓存。如果一个子目标已经被某个草图的 AlphaProof 搞定过，别的草图可以直接复用这个结果，不用再算一遍。

整套流程走下来，就是一个巨大的并行搜索——成百上千个"证明员"同时在草稿纸上写写画画，编译器是永不打盹的裁判。

📊 九个问题，三百块一个

论文的系统评估分两路走。

第一路：Erdős 问题。

从"形式猜想"仓库（Formal Conjectures）中选取当前已形式化的 353 个 Erdős 开放问题，全部喂给完整版智能体。每个问题最多跑 3000 轮。9 个被证出来了。

九个问题跨越数论、组合、加性组合。两个1968年的——56岁。一个1996年的——30岁。还有一个非 Erdős 本人之问却归入 Erdős 范畴的，同样被解决。

每道题的推理开销：几百美元（Gemini 3.1 Pro 的 API 调用费用为主，AlphaProof 每一题额外花约 ＄60 在 TPU 上）。

全部证明显式公开，成果已录入 Terence Tao 维护的"AI 贡献 Erdős 问题"wiki。

第二路：OEIS 猜想。

OEIS 是在线整数序列百科全书。论文用 Gemini 把 492 个未解决的 OEIS 猜想自动形式化成 Lean 语句，再喂给智能体。结果是 44 个被证明——人工审核确认，形式化正确且此前无人证过。

两个自不必说，放在补充材料里。其中一个涉及序列 A000045 的某种模性质，用归纳法一气呵成；另一个把组合生成函数和递推关系串联起来，手法干净。

🔬 实战：从优化到量子光学

论文的野心溢出 benchmark。作者把这套系统投进了真正的数学研究。

凸优化。智能体解决了一个悬而未决的收敛率问题：证明锚定梯度下降-上升（GDA）算法在 minimax 凸凹优化中可以达到 \(\mathcal{O}(1/t)\) 的精确收敛率，压紧了此前工作给出的更松上界。最妙之处——智能体证明了收敛率，更 自主发现了一个新的参数调度方案。人类给了它一个可调参数，标了 EVOLVE-VALUE。它搜了参数空间，找到了让证明成立的最优值。

代数几何。一个关于 Hilbert 函数的对数凹性问题，在余维度3、类型2的情形下悬了约15年。智能体把它证了。论证不短——需要非平凡地重构 Hilbert 函数、对不同情形逐类拆解二阶差分不等式。

图论。重构猜想的两个二分变体，智能体证了其中一个。一个关于生成树中叶子数上界的 Graffiti 猜想（1996年由自动猜想系统生成），证了。

加性组合。Ben Green 的著名开放问题列表里的 #57——关于两个二次函数空间的等价性——智能体未能直接证明。但它做了一件更聪明的事：用浮点数启发式搜索找到了一个反例（循环群 \(\mathbb{Z}/3\mathbb{Z}\)），然后证明了这个反例确实否证了原始猜想。问题变体被证伪，一篇独立论文在写。

量子光学。与 Mario Krenn 合作，解决了多个关于单色量子图存在性的猜想——\(N=d \in \{4,6,10\}\) 的情形悉数攻克，另有一篇论文在写。

⚡ 意外的温顺：基础版就够了？

论文里最让人沉默的一组数据，在消融实验里。

作者用事后分析的方式，把基础版（Agent A）、加 AlphaProof 版（Agent B）、加进化版（Agent C）、完整版（Agent D）全部拉回那9个已解决的 Erdős 问题，重跑对比。

结果惊了。基础版解开了全部9个。 对比完整版，差异不在"能不能解"，而在"花多少钱"。对简单题，基础版更便宜；对 #125 和 #138 这种硬骨头，完整版把推理成本砍到了原来的 1/2 到 1/5。

另一组数据：把 Gemini 3.1 Pro 换成更小的 Gemini 3.0 Flash 或 Gemini 3.1 Flash-Lite，以及让 AlphaProof 独自以树搜索模式运行——全部交白卷。

这意味着什么？LLM + 编译器反馈——一个简单到不能再简单的循环——在当前模型的能力等级上，已经可以用来攻克研究级数学问题。进化搜索、AlphaProof 加持、种群数据库——这些锦上添花的组件，在 LLM 能力继续增长的条件下，未来两年里重要性可能急剧下降。

这是这篇论文最锋利的观察：AI 做数学的重心，正在从"练一个专用的做题系统"滑向"用一个足够聪明的通用模型，配一个不会说谎的编译器"。

❓ 诚实的部分：哪些问题悬而未决

读完35页的论文，有些东西我确实不知道答案。

353个问题里解了9个——另外344个为什么没解？ 论文做了失败分析。最致命的失败模式：智能体把问题的核心难度悄悄塞进一个辅助引理里，然后给那个引理打上 sorry，假装它"是文献中已知的结果"。LLM 在压力下会编造引理——编得还很像真的。论文说提示里明令禁止这种行为了，没用。这是形式化方法和 LLM 不确定性之间一个尚未弥合的裂缝。

成本有水分。 论文给的"几百美元一个题"只算了成功解出的推理开销。但为了找到那9个可解的问题，智能体已经跑完了全部353个问题——每一道题都烧了钱。完整的探索成本远高于单题成功成本。论文在正文里坦白了这一点，但读者心里得有个数。

形式化和非形式化之间有隙。 把 Erdős 问题从自然语言翻译成 Lean，这件事本身就可能引入偏差。"密度"到底指"下密度"还是"自然密度"——论文里有两个问题是因为这个歧义被修正后才解出来的。智能体找到了"自然密度"版本的证明，提醒了人类原作者的形式化不够精确。这既是亮点，也是隐患：你怎么知道没被修正的那些问题，没有类似的歧义？

证明长什么样？ 智能体给出的 Lean 证明是机器可读的，配合补充材料里"去形式化"（deformalized）的自然语言版本，人类数学家才能看懂。但"去形式化"这一步——把 Lean 代码翻译回人类能读的证明——本身就可能引入误解。论文里提供了精选的自然语言证明，审得仔细。但没有对全部9个证明做同行评议。

领域偏好明显。 智能体擅长的——组合、数论、优化——恰好是 Lean 数学库（mathlib）最成熟的方向。代数几何做到余维度3就停了。复杂的拓扑、表示论、解析数论——论文没碰。这是工具成熟度施加的天花板，非LLM能力的天花板。

🦾 退一步：编译器是数学的测谎仪

这篇论文最根本的贡献，非"AI 解了 9 个 Erdős 问题"。这九题自有其价值。但更重要的，是它证明了一条路径的可行性——

用形式验证来驯服 LLM 的不确定性。

数学界对 AI 的最大忧虑，非"它会取代人类数学家"，实为"它会淹没人类数学界在看似正确、实则错误的论证里"。如果每一个 arXiv 提交日都收到几百篇 AI 生成的、有逻辑漏洞的"证明"，审稿系统就崩了。

形式化证明——编译器逐行验证——是应对这种危机的天然屏障。它在数学和 AI 之间放了一台测谎仪。LLM 可以说大话，可以编造引理，可以心虚时打 sorry——但编译器不认。编译不过的"证明"就是无效。

这篇论文让这个想法在开放问题上跑通了。九个问题，全部有完整的、可机器验证的 Lean 证明。你不需要信任 DeepMind。你只需要信任 Lean 编译器——而 Lean 编译器是开源的，任何人都可以自己验证。

这导向一个远得多的图景。如果形式化证明成为数学出版的常规格式——像今天的 LaTeX 一样普及——那 AI 和人类数学家在这条轨道上就平等了。 人写的证明也得走编译器。AI 写的证明也得走编译器。谁写的不重要，重要的是编译器的灯是绿还是红。

论文里有一句话，不显眼，但是这篇东西的注脚：

"Because the sketches were formal, experts could focus on the unresolved subgoals rather than re-verifying the entire argument."

证明是形式化的。人类专家不需要从头到尾重验——他们只需要看智能体没搞定的那部分。省下来的时间用在别的地方。

这，或许，比那九个 Erdos 问题本身的答案，更值得深思。

💭 尾巴：钱的那一边

最后一件事。

论文里反复出现一个词——cost。推理成本。计算成本。每个问题多少美元。优化目标和评估指标不是准确率，不是 pass@k，是花多少钱能解一道题。

读过几十篇 AI 论文，极少有人把"钱"当作核心指标来报告。通常的做法是比准确率——"我们比 baseline 高了 2.3 个百分点"——然后把这个数字写进表格，附一个小星号。至于高这两个百分点花了多少 GPU 时、多少电、多少美元——避而不谈。

这篇不回避。它把 Gemini 3.1 Pro 的 API 价格写进了附录，把 AlphaProof 的 TPU 耗时和单价列在实验部分，把完整版和基础版的每一分钱差距画进了成本-成功率散点图。每道题的平均推理开销、6题 × 4种智能体 × 多组并行度的成本表格——全部公开。

这不只关乎透明度。这关乎一个原则：数学是所有人的。 如果一个 AI 系统能证定理，但只有 Google 付得起运行它的账单——那它帮的不是数学，它帮的是富人的数学。

论文末尾提及，即便基础版 Agent A（LLM + 编译器循环，无需 AlphaProof 和进化搜索）也能解决所有9个问题。这意味着什么？意味着最便宜的版本，一个大模型 API 调用加上本地运行的开源 Lean 编译器——任何有几百美元预算的数学研究生都可以复制这个结果。

这是一个罕见的、把"可复现性"从一句口号变成一行金额数字的时刻。

📚 参考文献

1. Tsoukalas, G., Kovsharov, A., Shirobokov, S., et al. (2026). Advancing Mathematics Research with AI-Driven Formal Proof Search. arXiv:2605.22763.

2. Hubert, T., Schirrmacher, M., et al. (2025). AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems. Nature.

3. Novikov, A., Sener, O., et al. (2025). AlphaEvolve: Evolutionary Search for Scientific Discovery. arXiv.

4. de Moura, L., Kong, S., et al. (2015). The Lean Theorem Prover. CADE-25.

5. Feng, Y., et al. (2026). Aletheia: An AI Mathematician. arXiv.

#AlphaProofNexus #LeanTheoremProving #ErdosProblems #FormalVerification #AI4Math #DeepMind #智柴前沿实验室🎙️🚀