Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
Authors: name: Luoxin Chen; name: Jinming Gu; name: Liankai Huang; name: Wenhao Huang; name: Zhicheng Jiang; name: Allan Jie; name: Xiaoran Jin; name: Xing Jin; name: Chenggang Li; name: Kaijing Ma; name: Cheng Ren; name: Jiawei Shen; name: Wenlei Shi; name: Tong Sun; name: He Sun; name: Jiahui Wang; name: Siran Wang; name: Zhihong Wang; name: Chenrui Wei; name: Shufa Wei; name: Yonghui Wu; name: Yuchen Wu; name: Yihang Xia; name: Huajian Xin; name: Fan Yang; name: Huaiyuan Ying; name: Hongyi Yuan; name: Zheng Yuan; name: Tianyang Zhan; name: Chi Zhang; name: Yue Zhang; name: Ge Zhang; name: Tianyun Zhao; name: Jianqiu Zhao; name: Yichi Zhou; name: Thomas Hanwen Zhu
Published: 2025-07-31 17:00:30

Abstract: 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.