35/42，是一个很容易被写成“AI 奥数金牌”的数字。MiniMax-M3 团队在 arXiv 提交的 MaxProof 论文称，M3 在 IMO 2025 得到 35/42，在 USAMO 2026 得到 36/42，两个成绩都超过人类金牌阈值。

但这件事不能只按奖牌叙事读。它不是官方参赛获奖，也不能直接等同于“AI 已经会做数学研究”。真正值得盯住的是另一件事：数学证明正在从单模型答题，转向一套由算力、验证器和搜索策略驱动的工程系统。

MaxProof 交出的不是一次答题，而是一套证明搜索系统

论文标题是 《MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling》。arXiv 编号 2606.13473，提交时间是 2026 年 6 月 11 日。

几项关键信息压缩如下：

关键信息论文说法该怎么读
系统MaxProof，服务于 MiniMax-M3 系列不是单次问答，是证明搜索框架
成绩IMO 2025：35/42；USAMO 2026：36/42超过金牌阈值，但不是官方获奖认证
训练能力证明生成、证明验证、基于批评的证明修复模型不只写证明，还要挑错、改错
测试时机制同一模型充当 generator、verifier、refiner、ranker多候选证明竞争，再用 tournament selection 选最终证明
主要限制材料来自论文摘要和 arXiv 页面仍需看论文细节、评测设置和外部复核

论文里最关键的词不是 gold-medal threshold，而是 population-level test-time scaling。

翻译成人话：不要指望模型一次写出完美证明。让它生成一批候选，自己验证，自己批评，自己修复，再排序筛选。最后推出一个最能站住脚的版本。

这就把问题改写了。过去问的是“这个模型会不会做题”。现在要问的是“这个系统能不能把一堆半成品证明筛到足够可靠”。

真正的瓶颈，是别把错证明放过去

数学证明和普通问答不一样。普通问答错了，常常一眼能看出。证明错了，可能只差一步偷换概念，或者一个没补齐的“显然”。表面顺，里面空。

所以 MaxProof 的关键赌注是验证器。论文摘要提到 defense-in-depth generative verifier，目标是低误报率。这个目标很硬。验证器如果把错证明判成对，后面的搜索越努力，越可能把错误包装得更像真理。

这也是这类系统和“单模型灵光一闪”的区别：

路线主要依赖优点风险
单次生成模型一次推理能力简单、成本低、容易评估错误难自查，稳定性差
多候选搜索测试时算力、验证器、排序策略可反复试错，能放大正确候选成本上升，验证误报会被放大
MaxProof 这类闭环生成、验证、修复、排序合并系统性更强，能形成证明流水线泛化能力和复核成本还没结清

我更在意的是低误报。低误报不是漂亮指标，是整条流水线的闸门。

如果闸门不严，候选越多，错证明越多。修复越勤，幻觉越精致。最后排序选出来的，不一定是正确证明，也可能是最会骗过验证器的证明。

这对两类人有直接影响。

做 AI 数学和推理评测的团队，不能再只盯 pass@1 或最终得分。要把验证器误报率、候选数量、搜索轮次、失败样本审计放进评测表。否则看到的是成绩，不是能力结构。

准备采购或接入“数学推理工具”的企业，也别急着把它当自动数学家。更现实的动作是延后重决策，先要求供应方交代三件事：证明如何验证、每题搜索成本多高、有没有独立复核记录。没有这三项，分数再亮也只是演示材料。

我的判断：证明能力开始入厂，分数只是门面

这次 MaxProof 做对的一点，是没有把数学证明完全押在单模型智力上。它把证明拆成生成、质检、返工和选优。这个方向很像工业化。

历史上，工厂不是靠每个工人都变成天才取代手艺人。它靠流程、质检和规模，把原本稀缺的手艺拆开、复制、放大。数学证明当然不等于纺织机，这个类比只像三成。但重复的是同一种结构：谁能把稀缺能力拆成流程，谁就能放大它。

“天下熙熙，皆为利来。”放在这里不是说数学变俗了，而是说利益会流向能控制流程的人。能承担测试时算力，能训练验证器，能积累失败样本，能把修复闭环跑起来的组织，会比只发布一个强模型的组织更有优势。

代价也在这里。

第一，算力不再只是训练阶段的成本。测试时搜索本身开始变成能力的一部分。以后同一个底座模型，在不同算力预算下，可能表现出完全不同的“数学水平”。

第二，可验证性会变成商业分水岭。谁声称模型会证明，谁就要解释证明怎么验。只给最终答案，不给验证链路，很难让严肃用户买账。

第三，竞赛题和真实数学研究之间仍有距离。IMO、USAMO 题目有明确题面，也有相对清晰的评分框架。开放数学研究常常连问题如何形式化都还没定。MaxProof 的成绩能说明系统在竞赛证明上很强，但目前不能外推成“机器数学家已经到来”。

接下来最该看三件事：评测细节是否经得起复核，低误报验证器到底怎么定义和测试，测试时搜索的成本是否能被真实产品承受。

开头那个 35/42 很亮。亮到容易晃眼。真正该盯住的，是灯后面的发电厂：谁供电，谁验货，谁为每一次搜索买单。