字節跳動 Seed 團隊推出新一代形式化數學推理專用模型 Seed Prover 1.5，通過大規模的 Agentic RL 訓練，其推理能力和推理效率取得顯著進步。相比上一代模型，Seed Prover 1.5 在 16.5 小時內，針對 IMO 2025 的前 5 道題目生成了完整可編譯驗證的 Lean 證明代碼，換算成績為 35/42，達到此前 IMO 評分標準的金牌分數線。

更系統的評估中，Seed Prover 1.5 在完整的 Putnam 歷史評估集上解決了 88% 的問題，在代表碩士數學難度的 Fate-H 和代表博士生數學難度的 Fate-X 評估集上，分別解決了 80% 和 33% 的問題，刷新了形式化數學推理模型在這幾個評測集上的 SOTA 表現。

Seed Prover 1.5 針對 FATE-H 問題調用工具示例：

技術報告：https://arxiv.org/abs/2512.17260Lean
證明代碼：https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip