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

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.