AI结案56年悬案，赢的不止算力

数学界最难的考场，AI拿到了银牌；随后，一批悬置数十年的公开问题被它批量结案。

Google DeepMind 的 AlphaProof 在2024年国际数学奥林匹克（IMO）上解出6道题中的4道，达到银牌水平——这是AI首次在IMO这个人类最高强度的数学考场上拿到可查证的成绩，相关成果经同行评审后发表于《Nature》。此后，它又在数学家 Thomas Bloom 维护的 Erdős问题网站（erdosproblems.com）上，为多个悬置已久的公开问题给出了通过形式化验证的完整证明。

很多人把它读成“大模型更聪明了”。我不这么看。做数据平台这些年，我见过太多“模型很惊艳、工程一团糟”的demo。这次的胜负手，恰恰不在模型，而在一条跑通的可验证数据闭环——这才是值得数据行业认真拆解的东西。

🧮 过了同行评审，才算真的破门

数学界不认demo，只认能扛住审稿的证明。

先看事实本身。2024年7月，DeepMind公布 AlphaProof 与 AlphaGeometry 2 协作解出当届IMO 6道题中的4道——2道代数、1道数论由AlphaProof完整证明，1道几何由AlphaGeometry 2拿下。这不是发博客、跑个benchmark就完事：成果随后经同行评审发表于《Nature》，评审对象不是“解题思路”，是一条条用形式化语言写成、可被机器逐行校验的完整证明。这延续了DeepMind的路数——此前 AlphaGeometry 解几何题的成果，同样是走《Nature》同行评审发表的。

时间线其实很短，一句话就能拉完：2024年7月IMO考场拿成绩 → 《Nature》同行评审验收 → 2025年起在Erdős问题网站上批量结案悬置已久的公开问题。 Erdős问题网站收录了数学家Paul Erdős生前留下的一千多个公开问题，是全球数学家日常翻的真实研究题库——在那上面结案，不是玩具题。

技术底座说清楚：AlphaProof的语言模型基于 Gemini，负责把自然语言题目翻译成 Lean 形式化语言，再用类AlphaZero的强化学习在Lean环境里反复推演。这个组合的含义，我们后面细拆。

产业逻辑是什么？我认为关键不是“破题数量”，而是验收标准的切换。此前AI做数学，大多停留在“答案看起来对”——评测集泄露、答案碰瓷的争议从来没断过。这次，AI的数学产出第一次按人类学术界最高标准被完整验收。这意味着AI的输出第一次在“最不信任直觉”的领域拿到了通行证。

一位数学背景的朋友跟我说过一句大实话：数学界对“AI说它证明了”的默认反应，是当营销看。这次的差别在于，证明本身经得起逐行检查——而这要归功于下面那台“裁判机”。

🔁 Lean：给AI装了一台零成本裁判机

强化学习时代，最贵的不是算力，是能打分的裁判。

数据圈私下流传一句话：谁手里有便宜又诚实的裁判，谁就赢了这一轮RL。AlphaProof 的裁判，就是 Lean。

Lean是一门形式化语言。它的特别之处在于：一个数学证明被写成Lean代码后，对不对不需要任何“人”来投票——编译器逐行机械校验，通过就是通过，失败就是失败，没有任何模糊地带。审稿人可能看走眼，编译器不会。

这就补上了大模型做数学最致命的一环：奖励信号。通用文本上训练模型，对错靠人评，又贵又主观；而在Lean环境里，每一步推演都能被机器即时判定，模型可以反复试错、迭代，失败的分支立刻被剪掉，成功的证明被固化下来。

整条链路一句话拆开：模型生成候选证明 → Lean编译校验 → 通过则固化为样本入库，失败则带着精确的错误位置回炉重推。

注意那个从“校验失败”绕回“推演”的回路——这才是精华。每次失败不是浪费，而是给模型喂了一条带精确错误位置的负样本。训练信号在闭环里自产自销，不需要人工标注一枪一弹。

从工程视角算笔账：调用一次人类专家评审，成本以天和美元计；跑一次Lean编译校验，成本几乎可以忽略，且可以无限次重复、永不疲劳、永不徇私。当验证成本趋近于零，生成能力就会被指数级放大——这是所有做过数据质检的人都懂的基本盘，只不过这次是在数学上兑现了。

🗄️ 高纯度语料，才是稀缺燃料

互联网文本是贫矿，形式化证明是已经炼好的高纯度金属。

换到数据视角，这件事更有意思。我们天天喊“数据是燃料”，但燃料和燃料的纯度天差地别。拿三类语料对比一下：

最后一行就是Lean生态的真正价值：这个语料库里不存在“看起来对”的样本，每一条都过了机器校验。对训练来说，这等于跳过了数据清洗里最昂贵的环节——真伪判定。

而Erdős问题网站上的公开问题被批量结案，暴露了另一层逻辑：现成的“题库+验收标准”本身就是战略资产。猜想库提供目标，形式化环境提供裁判，模型提供劳动力——三者拼齐，闭环才能转起来。数学领域恰好三样都有，这就是为什么突破口出现在这里，而不是别的学科。

据我观察，不少团队还在用“爬更多网页”的思路堆数据。方向可能反了。在垂直领域，把领域知识形式化成机器可校验的规则，比多爬十个TB的原始文本值钱。前者是在铸造高纯度燃料，后者只是在扩库存。

对做数据平台的人，这是一个明确的信号：未来几年，最抢手的数据工程岗位，可能不再是ETL调优，而是“领域形式化”——把法务条款、财务准则、工程规范翻译成机器能校验的语言。

⚠️ 可验证性是分层的：数学是天花板，不是孤例

数学只是极端解法，但“分层验证”的思路到处都能降级使用。

有人会说：数学能完全形式化，我的业务场景没这条件。这话对了一半。可验证性本身是分层的：数学处在最高层——编译器逐行校验，错误无处遁形；代码和规则引擎处在中间层——跑一遍测试就能判大部分对错；再往下，大多数业务场景连“输出依据是什么”都没说清，就开始谈智能了。

所以这个案例真正的迁移价值，不是让每个行业都去学Lean，而是提醒你先给场景找一台尽可能硬的裁判：能形式化的形式化，能写测试的写测试，退而求其次也要把判定标准从“感觉对”推进到“有据可查”。裁判每往上抬一层，错误就少一个藏身之处。

📊 给数据平台人的三个落地判断

概念会退潮，闭环不会。

回到我们自己的饭碗。AlphaProof 这件事，对数据行业至少有三条可以直接落地的判断：

第一，验证器优先于生成器。 多数团队的惯性是先堆生成能力、后补质检。这次的结果再次证明顺序反了：Lean环境之所以能让模型反复推演，是因为裁判先于选手就位。企业内做AI应用，先问一句——你的场景里有没有一台“编译器”能机械判定输出对错？没有，先造这个，成本远低于再训一个模型。

第二，数据飞轮有了新形态。 老飞轮是“用户使用→数据回流→模型迭代”，卡在人工标注上。新飞轮是“模型生成→机器验证→合格样本入库沉淀”——像这次被证明的公开问题一样，每一轮解题都在给题库添砖。验证通过的证明沉淀为语