字节跳动Seed团队发布最新数学推理专用模型Seed Prover 1.5，在IMO 2025竞赛中取得金牌成绩。模型在16.5小时内解决前5道题目，获35分，达到今年IMO金牌线，与谷歌Gemini打平。前代模型当时仅获银牌成绩。

【核心创新】

1. Agentic Prover：新型形式化数学推理范式，将Lean语言视为工具，模型可自主调用多种工具：Mathlib搜索工具（检索定理和定义）、Python代码执行（辅助验证）、增量式引理验证（将复杂问题拆解为引理逐步证明）。
2. Sketch Model：自然语言到形式语言的翻译器，模拟人类数学家先写非形式化证明草稿的方式，将复杂命题转化为难度更低的子目标，专注于逻辑路径规划而非语法细节。

【Scaling验证】

模型采用大规模强化学习训练，实验证明随着RL训练步数增加，证明通过率从50%升至接近90%。同时验证了测试时Scaling的有效性：增加推理阶段计算资源可显著提高解题率。

【性能表现】

除IMO外，模型在北美本科级别数学竞赛Putnam基准上也大幅刷新SOTA成绩。技术报告已公开，模型尚未开源。