字节跳动 Seed 团队发布形式化数学推理模型 Seed Prover 1.5，采用 Agentic 架构支持 Mathlib 搜索、Python 执行与增量引理验证，并引入 Sketch Model 将复杂证明拆解为子引理并行攻克。基于大规模 Agentic RL 训练，该模型在 16.5 小时内完成 IMO 2025 前 5 题获 35/42 分（金牌线），9 小时内解决 Putnam 2025 的 11/12 题，在 Putnam 历史集、Fate-H 和 Fate-X 上分别达 88%、80% 和 33% 通过率，刷新多项 SOTA。