在人工智能向人类智慧所有领域发起挑战的宏大叙事中，数学，尤其是奥林匹克级别的数学竞赛，始终被视为那座最陡峭、也最神圣的“哥德巴赫猜想”式山峰。它考验的不仅是计算能力，更是抽象、直觉与构建精妙证明的艺术——这些长期被认为是人类独有的天赋。
然而，近日字节跳动Seed AI团队发布的Seed Prover 1.5模型，以及它在国际数学奥林匹克（IMO）模拟赛中斩获金牌的战绩，正以一种不容辩驳的方式，宣告着这座山峰的最后一道防线正在被突破。
这并非又一个依靠算力堆砌出的高分。Seed Prover 1.5在16.5小时内解决了IMO 2025的前五道题，最终以35分的成绩与谷歌Gemini并驾齐驱，这一成就的背后，是一场深刻的方法论革命。它标志着AI正从一个只会遵循严格语法的“形式逻辑学家”，进化为一个懂得规划、懂得使用工具、甚至懂得“打草稿”的、真正的“问题解决者”。
从“银牌”到“金牌”：强化学习的暴力跃迁
字节跳动上一个版本的模型，需要耗时三天才能解出四道题，最终仅获银牌。而Seed Prover 1.5的飞跃，其核心驱动力之一，是对大规模强化学习的极致运用。
通过海量的自我博弈与训练，模型在证明题上的成功率，从最初的50%戏剧性地跃升至接近90%。
这不仅是量的积累，更是质的蜕变。AI不再是漫无目的地在无穷的可能性空间中进行搜索，而是通过强化学习，学会了某种接近人类数学家的“题感”——一种对有效证明路径的直觉判断力。这种能力的提升，也让它在同样以高难度著称的北美数学竞赛Putnam中，刷新了历史最佳成绩。
AI的两件“法宝”：当机器拥有了图书馆与草稿纸
Seed Prover 1.5的技术报告，揭示了两项极具开创性的创新，它们共同构成了其强大推理能力的基石。
第一件法宝，是Agentic Prover——一个懂得使用工具的“行动派”。
传统AI进行数学推理，要么使用自然语言（模糊但不严谨），要么使用像Lean这样的形式化语言（严谨但极难掌握）。Agentic Prover选择并攻克了更具挑战性的后者。它不再是一个封闭的“大脑”，而是被赋予了与外部世界交互的能力。当推理陷入僵局时，它可以主动调用多个工具：
-
它可以像一个研究者一样，去检索庞大的Lean数学库Mathlib，寻找可以引用的现成定理。
-
它也可以像一个工程师一样，编写并运行Python脚本，去完成复杂的数值计算或验证猜想。
这从根本上改变了AI的角色，使其从一个纯粹的“思考者”，变为一个手握工具箱的“实干家”。
第二件法宝，是Sketch Model——一个拥有“草稿纸”的“战略家”。
这或许是此次突破中最接近人类思维精髓的部分。顶尖的数学家在解决一个复杂问题时，并非从第一行开始就书写完美无瑕的形式化证明。他们会先在脑中或纸上进行非正式的、高度抽象的“草稿”推演——勾勒出核心思路，列出可能需要的关键引理，搭建起整个证明的逻辑框架。
Sketch Model正是对这一过程的精妙模拟。它允许AI先生成一份非正式的证明草稿，用更自由的语言规划出整体的解题路径。随后，系统再将这份“草稿”作为详细的路线图，引导模型一步步将其转化为严谨的、可被计算机验证的形式化证明。
通过一种混合奖励信号的强化学习策略，Sketch Model不仅极大地提升了AI对复杂问题的宏观规划能力，更重要的是，它将一个几乎不可能完成的“一步登天”式任务，分解为了“先画蓝图，再施工”的、更符合认知规律的两阶段过程。
远瞻：从解题到发现，数学研究的新范式
Seed Prover 1.5的成功，其意义远不止于赢得一枚虚拟的金牌。它为我们揭示了一个全新的可能性：
在不远的未来，AI将不再仅仅是验证人类数学家猜想的工具，更有可能成为一个平等的、甚至能提出深刻洞见的“合作者”。它能够处理人类因精力有限而无法企及的、极其庞大和复杂的证明，甚至在海量数据中发现全新的数学模式与关联。
在教育领域，一个能够理解学生“草稿”思路、并能提供启发式指导的AI导师，将彻底改变数学教育的方式。它不仅能判断对错，更能理解过程，因材施教。
当然，IMO的最后一题，Seed Prover 1.5依然未能解出，这恰恰说明了人类最顶尖的、那种天马行空般的创造力，至今仍是AI尚未完全征服的圣域。但这枚金牌已经证明，AI正在以一种令人敬畏的速度，学习着人类最古老、也最高贵的思维艺术。一场人与机器在纯粹理性王国中的伟大合作，其序幕正在缓缓拉开。
论文地址：https://arxiv.org/pdf/2512.17260
