Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

TL;DR

Seed-Prover is a novel formal reasoning system that iteratively refines proofs using Lean feedback, achieving state-of-the-art results on IMO problems and introducing a geometry engine for formal geometry reasoning.

Contribution

We introduce Seed-Prover, a lemma-style proof model with iterative refinement and test-time strategies, plus Seed-Geometry for formal geometry reasoning, advancing automated theorem proving.

Findings

Proves 78.1% of IMO problems formally

Achieves over 50% on PutnamBench

Outperforms previous state-of-the-art methods

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 \textbf{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 \textbf{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.