Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
LLMs have demonstrated strong mathematical reasoning abilities by leveraging
reinforcement learning with long chain-of-thought, yet they continue to
struggle with theorem proving due to the lack of clear supervision signals when
solely using natural language. Dedicated domain-specific languages like Lean
provide clear supervision via formal verification of proofs, enabling effective
training through reinforcement learning. In this work, we propose
Seed-Prover, a lemma-style whole-proof reasoning model. Seed-Prover
can iteratively refine its proof based on Lean feedback, proved lemmas, and
self-summarization. To solve IMO-level contest problems, we design three
test-time inference strategies that enable both deep and broad reasoning.
Seed-Prover proves 78.1% of formalized past IMO problems, saturates MiniF2F,
and achieves over 50\% on PutnamBench, outperforming the previous
state-of-the-art by a large margin. To address the lack of geometry support in
Lean, we introduce a geometry reasoning engine Seed-Geometry, which
outperforms previous formal geometry engines. We use these two systems to
participate in IMO 2025 and fully prove 5 out of 6 problems. This work
represents a significant advancement in automated mathematical reasoning,
demonstrating the effectiveness of formal verification with long
chain-of-thought reasoning.
688c16788c434640078cc348
Luoxin Chen
688c16788c434640078cc349
Jinming Gu
688c16788c434640078cc34a
Liankai Huang
688c16788c434640078cc34b
Wenhao Huang
688c16788c434640078cc34c
Zhicheng Jiang
688c16788c434640078cc34d
Allan Jie
688c16788c434640078cc34e
Xiaoran Jin
688c16788c434640078cc34f
Xing Jin
688c16788c434640078cc350
Chenggang Li
688c16788c434640078cc351
Kaijing Ma
688c16788c434640078cc352
Cheng Ren
688c16788c434640078cc353
Jiawei Shen
688c16788c434640078cc354
Wenlei Shi
688c16788c434640078cc355
Tong Sun
688c16788c434640078cc356
He Sun
688c16788c434640078cc357
Jiahui Wang
688c16788c434640078cc358
Siran Wang
688c16788c434640078cc359
Zhihong Wang
688c16788c434640078cc35a
Chenrui Wei
688c16788c434640078cc35b
Shufa Wei
688c16788c434640078cc35c
Yonghui Wu
688c16788c434640078cc35d
Yuchen Wu
688c16788c434640078cc35e
Yihang Xia
688c16788c434640078cc35f
Huajian Xin
688c16788c434640078cc360
Fan Yang
688c16788c434640078cc361
Huaiyuan Ying
688c16788c434640078cc362
Hongyi Yuan
688c16788c434640078cc363
Zheng Yuan
688c16788c434640078cc364
Tianyang Zhan
688c16788c434640078cc365
Chi Zhang
688c16788c434640078cc366
Yue Zhang
688c16788c434640078cc367
Ge Zhang
688c16788c434640078cc368
Tianyun Zhao
688c16788c434640078cc369
Jianqiu Zhao
688c16788c434640078cc36a
Yichi Zhou
688c16788c434640078cc36b
Thomas Hanwen Zhu
Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
LLMs have demonstrated strong mathematical reasoning abilities by leveraging
reinforcement learning with long chain-of-thought, yet they continue to
struggle with theorem proving due to the lack of clear supervision signals when
solely using natural language. Dedicated domain-specific languages like Lean
provide clear supervision via formal verification of proofs, enabling effective
training through reinforcement learning. In this work, we propose
Seed-Prover, a lemma-style whole-proof reasoning model. Seed-Prover
can iteratively refine its proof based on Lean feedback, proved lemmas, and
self-summarization. To solve IMO-level contest problems, we design three
test-time inference strategies that enable both deep and broad reasoning.
Seed-Prover proves 78.1% of formalized past IMO problems, saturates MiniF2F,
and achieves over 50\% on PutnamBench, outperforming the previous
state-of-the-art by a large margin. To address the lack of geometry support in
Lean, we introduce a geometry reasoning engine Seed-Geometry, which
outperforms previous formal geometry engines. We use these two systems to
participate in IMO 2025 and fully prove 5 out of 6 problems. This work
represents a significant advancement in automated mathematical reasoning,
demonstrating the effectiveness of formal verification with long
chain-of-thought reasoning.
Seed-Prover, a lemma-style reasoning model using Lean, achieves high performance in formal theorem proving and automated mathematical reasoning through iterative refinement and specialized geometry support.
reinforcement learning long chain-of-thought theorem proving formal verification lemma-style reasoning Seed-Prover MiniF2F PutnamBench Seed-Geometry automated mathematical reasoning