%20--%3e%3cdefs%3e%3cstyle%3e%20.st0%20{%20fill:%20%23061b40;%20}%20.st1%20{%20fill:%20%23306af1;%20}%20.st2%20{%20fill:%20%235ce5cf;%20}%20%3c/style%3e%3c/defs%3e%3cg%3e%3cpath%20class='st0'%20d='M55,10.5h9v3h-9v9h12V7.5h-12v3ZM64,19.5h-6v-3h6v3Z'/%3e%3cpolygon%20class='st0'%20points='69%2016.5%2078%2016.5%2078%2019.5%2069%2019.5%2069%2022.5%2081%2022.5%2081%2013.5%2072%2013.5%2072%2010.5%2081%2010.5%2081%207.5%2069%207.5%2069%2016.5'/%3e%3cpolygon%20class='st0'%20points='95%2010.5%2095%207.5%2083%207.5%2083%2022.5%2095%2022.5%2095%2019.5%2086%2019.5%2086%2016.5%2095%2016.5%2095%2013.5%2086%2013.5%2086%2010.5%2095%2010.5'/%3e%3cpath%20class='st0'%20d='M40,1.5v21h11.6l1.4-1.4v-7.6h0c0,0-1.4-1.5-1.4-1.5l1.4-1.4V2.9l-1.4-1.4h-11.6ZM50,19.5h-7v-6h7v6ZM50,10.5h-7v-6h7v6Z'/%3e%3c/g%3e%3cpath%20class='st1'%20d='M23.1,24L14.7,4.8l-4.9,11.2h3.8l-1.8,4H3.3L12.1,0H2C.9,0,0,.9,0,2v20c0,1.1.9,2,2,2h21.1Z'/%3e%3cpath%20class='st2'%20d='M34,0h-16.8l10.6,24h6.2c1.1,0,2-.9,2-2V2C36,.9,35.1,0,34,0ZM32.5,20h-4V4h4v16Z'/%3e%3c/svg%3e)
Recently, the Seed AI team under ByteDance released a mathematical reasoning model called Seed Prover 1.5. The model performed exceptionally well in the International Mathematical Olympiad (IMO), successfully winning a gold medal, marking another breakthrough in artificial intelligence within the field of mathematics.
Seed Prover 1.5 adopted the Scaling Law theory and solved the first five problems of IMO2025 within 16.5 hours, missing only one question and achieving a score of 35, which met the gold medal standard. This performance is on par with Google's Gemini, while ByteDance's previous model took three days to complete four questions and ultimately earned a silver medal. Clearly, Seed Prover 1.5's performance has set a new benchmark for AI mathematical reasoning models.
The success of this model is not accidental. Its core lies in the introduction of large-scale reinforcement learning. Through training, the model's success rate in proving problems increased from an initial 50% to nearly 90%. In addition, Seed Prover 1.5 also set a new record in the North American mathematics competition Putnam, demonstrating its strong problem-solving capabilities.
In the technical report of Seed Prover 1.5, two important innovations were introduced: Agentic Prover and Sketch Model. Agentic Prover adopts a new formal mathematical reasoning approach, using formal languages such as Lean to create verifiable proofs. This method is more rigorous than traditional natural language reasoning but also more challenging. To overcome this difficulty, Seed Prover 1.5 allows the model to call multiple tools during the reasoning process, such as retrieving the Lean mathematical library Mathlib and writing Python scripts for calculations.
The Sketch Model was designed to help the model better "draft" solutions. This model simulates the thinking process of human mathematicians, allowing it to first make informal proof drafts, list key lemmas and ideas, and then convert them into formal proofs. Through a mixed reward signal reinforcement learning strategy, the Sketch Model not only improves overall logical planning ability but also effectively reduces the difficulty of complex problems.
In summary, Seed Prover 1.5 not only demonstrates ByteDance's innovation and strength in the field of AI mathematical reasoning, but also provides new possibilities for future mathematical research and education.
Paper link: https://arxiv.org/pdf/2512.17260