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
claimed_verified
2025-08-06T19:31:07.060Z
5f729da2f1e7ef6e919a1c27
/avatars/bdf48f0d3290fab54d7e9636a3d14158.svg
Zhanming (Allan) Jie
user
allanjie
688c16788c434640078cc34e
Xiaoran Jin
688c16788c434640078cc34f
Xing Jin
688c16788c434640078cc350
Chenggang Li
688c16788c434640078cc351
Kaijing Ma
688c16788c434640078cc352
Cheng Ren
688c16788c434640078cc353
Jiawei Shen
688c16788c434640078cc354
Wenlei Shi
claimed_verified
2025-08-06T19:31:02.757Z
6471a24381ded91f253ceb1c
https://cdn-avatars.huggingface.co/v1/production/uploads/no-auth/eNBQ29BIH4EUx7JYF30p4.png
Wenlei Shi
user
WesleyShi
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
claimed_verified
2025-08-06T19:31:09.979Z
5f694b8b5e78cc6b0ed31bd2
/avatars/63f21d30918c34fff9ea592e1039b3f0.svg
Zheng Yuan
user
GanjinZero
688c16788c434640078cc364
Tianyang Zhan
688c16788c434640078cc365
Chi Zhang
688c16788c434640078cc366
Yue Zhang
688c16788c434640078cc367
Ge Zhang
claimed_verified
2025-08-13T07:29:37.057Z
638efcf4c67af472d316d424
/avatars/97a57859d7d87a3a8f1bb41d32a72bc2.svg
Ge Zhang
user
zhangysk
688c16788c434640078cc368
Tianyun Zhao
688c16788c434640078cc369
Jianqiu Zhao
688c16788c434640078cc36a
Yichi Zhou
688c16788c434640078cc36b
Thomas Hanwen Zhu
claimed_verified
2025-08-06T19:31:13.245Z
654ac8b57ed5797e22eb85e2
/avatars/cb618f9e69ca0362a35b2f1bf4050064.svg
Thomas Zhu
user
hanwenzhu
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