分数和金牌线都核实了，但有三处口径要拧紧
先纠一个会让人找错论文的错：帖子给的 arXiv 编号不对。2509.05823 是 Datta 和 Polson 的统计学论文（Tweedie 公式那篇），跟数学奥赛毫无关系。真号是 2609.10712（Moshkov, Ge, Armstrong, Du, Mahdavi, Gitman，2026-09-09）。
核对过原文，摘要本身很老实：30/42 分，P1、P2、P4、P5 四个 7 分满分，P3、P6 各得 1 分；金牌线 29 分也两个外部来源都证实了——IMO 官网第 67 届页面（上海，117 国 666 人，55 金）和英国 UKMT 的官方通报都写着 29/23/16 三条奖牌线。
但有三处口径，转载的时候一并带上会更准确：
一、"获得 IMO 金牌"这个说法过界了。 IMO 官方成绩册里没有任何 AI 条目，金银铜牌授予的是各国代表队选手。准确的说法是"在 IMO 2026 官方赛题、官方 4.5 小时赛制、官方阅卷人批改下取得 30/42，超过 29 分金牌线"。30 分只超线 1 分，属于擦线。
二、把算力一起报，这个成绩才是完整的。 系统是三个 Nemotron-3-Ultra 550B-A55B 检查点（通用版 + SFT + RL 两个专家），每题第一轮就采样 384 个证明尝试，最多跑 8 轮。找到 6 份提交解答花了约 707M 生成 token、1,464 个 GB200 GPU 小时；完整赛程约 2.31B token、4,800 GPU 小时；P6 赛后又补跑 610M token、890 GPU 小时。"无形式化证明器、无外部工具"的另一面是这个量级。论文顺手把资源核算也发布了，这事值得夸——大部分同类工作只报分数不报账。
三、模型自评和官方阅卷差了 2 分，而且差得有规律。 内部两个 verifier 在比赛截点估的是约 32 分，比官方 30 分高出的 2 分全在 P3 和 P6——都是模型评审给了满分、官方只给 1 分的题。论文自己称之为 model-based verification 的 shared blind spot。更巧的是，搜索期的验收标准也是模型：16 个判断全部给 1 才收。自己出的考卷自己批，这两分就是代价。 另外流传的"33 分"是非官方版本——P6 在赛后 8 小时 25 分找到新解，人类数学家评了 4/7，但论文脚注明确排除（无官方评分标准，P3 也没改善）。
还有两处细节：消融实验只用了一个 30 题开发集（3 easy / 7 medium / 10 hard / 10 unsolved），因为 200 题的 Nemotron-IMO-Bench 跑全量高算力管道太贵；跨年对比要当心——2024 是 AlphaProof 加 AlphaGeometry 2 组合差金牌线 1 分，2025 是 Gemini Deep Think 和 OpenAI 实验模型达到金牌级，三届赛题、奖牌线、算力预算都不同，摆进同一张排行榜是不公平的。
值得肯定的是它的坦诚：triage 路由会丢掉后续被证明正确的候选（人类复审 14 个里 13 个全对），所以生产系统弃用了；§7.4 明说几种花哨的 refinement 策略 none improved final aggregate performance；两个后训练检查点、训练数据、代码、提交的解答全部开源。
一句话：这是一次货真价实的官方赛制成绩，配得上一个可复现的参照系——只是下次转述时，把"官方阅卷下的 30/42"和"四千八百个 GB200 小时"放在同一句里，比单说"IMO 金牌"诚实得多。
