【#Tech24H】On December 24, ByteDance’s Seed team announced the launch of its next-generation formal mathematics reasoning model, Seed Prover 1.5. Through large-scale Agentic Reinforcement Learning training, the model has achieved notable improvements in reasoning capability and efficiency. Compared to its predecessor, Seed Prover 1.5 generated complete, compilable, and verifiable Lean proof code for the first five problems of the IMO 2025 within 16.5 hours, a score of 35 out of 42, reaching the gold medal threshold under previous IMO scoring standards. The technical report for Seed Prover 1.5 has been publicly released, and APIs will be made available subsequently, inviting interested mathematics and AI researchers to experience the model.