Agents2025~129 minarXiv:2512.17260

Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience

score 8Jiangjie Chen, Wenxiang Chen, Jiacheng Du +19ByteDance Seed↑ 52Dec 19, 2025cs.CL

🎯 Pitch

An agentic Lean prover trained via large-scale reinforcement learning solved 11 of 12 problems from the Putnam 2025 competition in just 9 hours, shattering the computational efficiency barrier that previously made formal theorem proving orders of magnitude more expensive than natural-language reasoning. Seed-Prover 1.5 achieves this by learning optimal interactions with Lean and auxiliary tools from high-quality formal feedback during training, establishing that experiential RL can close the gap between formal verification and the performance of natural-language proof systems.

1. Executive Summary

This paper introduces Seed-Prover 1.5, a formal theorem-proving system that combines an agentic Lean prover trained via large-scale reinforcement learning with a sketch model that bridges natural-language proofs and formal Lean code, evaluated on PutnamBench, FATE, CombiBench, IMO 2025, and Putnam 2025. The core technical mechanisms are agentic reinforcement learning (the prover dynamically interacts with Lean, mathlib search, and Python execution, learning adaptive tool-use strategies and incremental lemma caching) and rubric-based reward modeling for sketch training (an LLM-as-a-Judge evaluates lemma decomposition quality using a structured rubric, producing a binary reward that drives VAPO-based RL). The system achieves state-of-the-art performance with a moderate compute budget, solving 88% of PutnamBench (undergraduate-level), 80% of Fate-H (graduate-level), and 33% of Fate-X (PhD-level) problems — crucially solving 11 out of 12 Putnam 2025 problems within 9 hours, establishing that formal proving can approach natural-language reasoning capability at the undergraduate and graduate levels only when the system learns from experience through high-quality formal feedback rather than relying on monolithic single-pass generation.

2. Context and Motivation

The Core Problem: Formal Theorem Proving Remains Vastly More Expensive Than Natural-Language Reasoning

The central tension this paper addresses is a striking asymmetry in modern AI for mathematics. On one side, large language models have achieved remarkable success at natural-language mathematical reasoning: DeepSeek-Math-V2 [20] scored near-perfectly on the Putnam 2024 competition, and systems like InternLM-Math [30] and Gao et al. [5] have pushed the frontier of rigorous informal proofs. On the other side, formal theorem proving — where proofs are written in machine-checkable languages like Lean 4 [15] — remains stubbornly difficult and computationally prohibitive, especially for undergraduate-level mathematics and beyond.

The gap is quantified starkly in the introduction. While DeepSeek-Math-V2 achieved near-perfect performance on Putnam 2024 in natural language, AlphaProof [8] — the state-of-the-art formal prover at the time — solved only 56% of the full PutnamBench (a benchmark that is on average simpler than the 2024 competition set). Even more tellingly, AlphaProof consumed approximately 500 TPU-days per problem — a computational cost that makes formal proving orders of magnitude more expensive than the natural-language alternative. The paper frames this as an existential challenge for the field:

"If LLMs can achieve high rigor in natural language proof, while formal proof continues to impose a heavy performance tax, one might question: Is pursuing formal theorem proving with LLMs still a viable and valuable path?"

This framing is critical because it acknowledges head-on that formal proving is losing the efficiency race to natural-language methods — not in terms of trustworthiness (formal proofs are guaranteed correct; natural-language proofs are not), but in terms of capability-per-dollar. The paper's answer to this question is a qualified "yes," but only if we fundamentally rethink how LLMs interact with proof assistants and how they learn from those interactions.

Why Formal Proving Matters Despite the Efficiency Gap

The authors argue that formal theorem proving remains worth pursuing for three interlocking reasons, only one of which is explicitly stated in the introduction but all of which emerge across the paper:

1. Trustworthy verification without hallucination risk. Lean provides fully mechanical verification: a proof that passes the compiler is logically sound with respect to the formalized definitions. Natural-language proofs, no matter how rigorous they appear, can contain subtle gaps, hidden assumptions, or outright errors that escape human and LLM scrutiny. For mathematics — where a single false lemma can cascade into an entire edifice of incorrect results — this guarantee is not a luxury; it is a necessity if LLMs are to be used as genuine mathematical assistants rather than merely pattern-matchers producing plausible-looking arguments.

2. Lean as an environment for learning from experience. Unlike natural-language proving, where feedback is either nonexistent or requires expensive human labeling, Lean provides a fully verifiable environment with ground-truth feedback. Every proof attempt receives a binary signal: it compiles (correct) or it doesn't (incorrect, with specific error messages). This makes Lean uniquely suited for large-scale reinforcement learning, where the agent can freely explore, accumulate experience, and iteratively improve without human intervention. The paper argues this environment is underutilized by current approaches that treat the interaction with Lean too coarsely or too finely — a point we will develop below.

3. Potential for genuine mathematical contributions. The paper's motivating vision — stated explicitly in the conclusion — is not merely solving competition problems for benchmarking purposes, but eventually contributing to frontier mathematical research. The authors tested their system on the Erdős problem set and solved 15 problems (e.g., Erdős-124, 198, 303). However, they caveat that these are "mathematically relatively simple" or involve simplified/misformalized versions of the conjectures. The honest admission that "our systems... are still some distance away from truly helping to advance research on frontier open mathematical problems" sets a realistic baseline while motivating the paper's core contribution: the scaling methodology might eventually bridge this gap if the "dependency issue" in mathematical research (identifying relevant prior work, grounding proofs in existing literature, and formalizing that literature) can be addressed.

Where Prior Approaches Fall Short: The Interaction Granularity Problem

The paper organizes prior work into two broad paradigms and argues that both suffer from inefficient interaction with the Lean environment:

Step-level provers [1, 8, 25, 27, 28] generate a single tactic at each step, interacting with Lean after every atomic operation. This gives the model fine-grained control and step-by-step feedback, but the interaction overhead is enormous: hundreds or thousands of round-trips per proof, with context windows accumulating state across every step. The paper notes this leads to computational inefficiency because the model "interacts too frequently" — every simp, rw, or apply triggers a separate API call, meaning a proof of moderate complexity requires the model to maintain coherence across an extremely long dialogue.

Whole-proof provers [3, 9, 12, 13, 18, 19, 23, 26, 33] take the opposite extreme: they generate the entire Lean proof in a single output, interact with the compiler once, and receive a pass/fail verdict with error messages. This reduces interaction overhead to a single round-trip, but it creates a severe context and reasoning problem: the model must anticipate all correctness requirements at once, cannot recover from mid-proof errors without regenerating the entire proof, and cannot incrementally cache verified intermediate results. The paper notes this makes the model "interact too sparsely" — error feedback arrives only after the entire proof is generated, making it difficult to localize and fix mistakes.

The paper identifies specific limitations in prominent prior systems:

AlphaProof [8]: Achieved olympiad-level formal reasoning, but at 500 TPU-days per problem and only 56% on PutnamBench. The step-level interaction paradigm was a bottleneck, and the system relied on massive computational resources to brute-force search over proof strategies.
Seed-Prover 1.0 [3]: The authors' own prior work, which introduced lemma-style proof decomposition and a "medium workflow" that consumed 18 H20-days per problem to solve 50% of PutnamBench. This system used whole-proof generation with post-hoc decomposition, but lacked dynamic tool interaction and suffered from the inefficiency of regenerating complete proofs.
Hilbert [22]: Used a powerful general reasoning model for informal proving and a specialized Lean model for formal verification, achieving 70% on PutnamBench with an average of 1840 attempts per problem. The paper acknowledges this as strong performance but critiques the paradigm: a two-model pipeline where formal proving is divorced from the reasoning process, with the formal prover essentially acting as a translator rather than a reasoning agent in its own right.
Aleph Prover: Required an average of 1834 tool calls per problem to achieve 75.8% on PutnamBench, suggesting that even with sophisticated search strategies, the interaction overhead remained high.

The Missing Paradigm: Agentic Reinforcement Learning in Formal Environments

The paper's key positioning claim in Section 3.1 is that both prior paradigms fundamentally misrepresent how a competent human uses a proof assistant. A human mathematician doesn't run Lean after every rw command, nor do they write a 1000-line proof in a text editor and submit it once at the end. Instead, they work at the granularity of lemmas and sub-goals: they prove a useful intermediate fact, verify it compiles, cache it, and use it as a building block for larger arguments. They dynamically search for relevant theorems in the standard library (mathlib), test conjectures with quick computations, and adjust their strategy based on partial feedback.

The agentic prover described in Section 3.1 is designed to operate at precisely this intermediate granularity. It generates lemmas (not individual tactics, not whole proofs), submits them to Lean for verification, caches successful lemmas for reuse, and can interleave mathlib searches and Python computations within the proving trajectory. This is not a small architectural tweak — it is a different interaction paradigm that the paper argues is both more capable and more efficient than prior approaches.

Critically, this paradigm requires the model to learn when to use tools, how to use them, and what granularity to work at — skills that cannot be effectively programmed in a static prompt or learned from SFT alone. The paper's second major positioning claim is that large-scale RL in this environment is underexplored frontier territory:

"training such an agentic prover via large-scale RL remains an underexplored frontier area. In this work, we demonstrate the scaling potential of this approach."

This sets up the paper's primary innovation: using VAPO-based reinforcement learning [31] with outcome-based rewards (+1 for a verified proof, −1 otherwise) to train the agentic prover to develop optimal interaction strategies, tool usage patterns, and adaptive search behavior through extensive interaction with the Lean environment and its associated tools.

The Natural-to-Formal Bridging Problem

Even with an efficient agentic prover, there remains a representation gap between how humans (and LLMs) reason about mathematics in natural language and how proofs are expressed in Lean. Natural-language proofs operate at a high level of abstraction, referencing mathematical concepts, making intuitive leaps, and structuring arguments as narratives. Lean proofs, even at their most elegant, require explicit type-theoretic justification for every step.

Prior approaches to bridging this gap fall into two categories, both of which the paper considers insufficient:

Monolithic formalization: Ask the LLM to directly translate a natural-language proof into Lean code. This was the approach in Seed-Prover 1.0 [3] and DeepSeek-Prover series [18, 26]. The problem is that the LLM must simultaneously decompose the proof strategy and handle low-level formal syntax in a single generation — a task that overwhelms the context window and produces brittle results for complex proofs.
Step-by-step translation: Translate each natural-language sentence into one or more Lean tactics. This is the approach implicitly used in Hilbert [22] and others. The problem is that the natural decomposition of the proof (into lemmas, subgoals, and intermediate claims) does not map cleanly to the tactical decomposition required by Lean, resulting in proofs that are fragile or miss the high-level structure.

The paper's sketch model (Section 3.3) occupies a distinctive middle position: it translates a natural-language proof into a lemma-style Lean sketch — a structured decomposition where the main theorem body shows how lemmas assemble into the final result, and each lemma is an independent sub-goal (initially admitted with sorry). This is not a full proof; it is a proof plan that the agentic prover can then attempt to discharge. The key insight is that evaluating sketch quality is a different problem from evaluating proof correctness: a sketch is good if its lemmas are mathematically valid and each lemma is strictly easier to prove than the original theorem, creating a genuine decomposition into simpler sub-problems.

Training such a model requires a reward signal beyond Lean verification alone (since the lemmas have sorry, the sketch doesn't compile). The paper's rubric-based RL approach (Section 3.3, detailed in Appendix B) uses an LLM-as-a-Judge with a structured rubric to evaluate sketch quality across multiple dimensions — alignment with the natural-language proof, decomposition granularity, difficulty reduction, and junk value analysis — fusing these into a binary reward that drives RL training. This is significant because it represents a methodology for training models on tasks where the ultimate correctness signal is unavailable or too expensive, using learned evaluators that generalize better than scalar reward models.

Reconciling Conflicting Prior Evidence

The paper emerges against a backdrop of seemingly contradictory evidence about whether RL helps for formal theorem proving. On one side, systems like AlphaProof [8] and DeepSeek-Prover-V2 [18] have shown substantial gains from RL training on formal proof data. On the other side, the field has been cautious: formal proof environments are sparse (most proofs fail), the reward signal is binary and delayed, and exploration is combinatorially challenging — making it unclear whether RL would scale or plateau after modest improvements.

The paper's positioning on this is empirical rather than theoretical. The training dynamics shown in Figure 3a — RL training accuracy increasing from approximately 50% to nearly 90% over 1200 training steps, with corresponding gains on held-out benchmarks (Figure 3b) — provide direct evidence that RL does scale for agentic proving when the environment, reward, and training data are appropriately designed. This is not a trivial result; it required careful curation of the training dataset (filtering examples provable by the SFT model to focus RL on challenging instances), a stable RL algorithm (VAPO [31] with tool-integrated reinforcement learning following ReTool [4]), and a continuous feedback loop where the model learns from thousands of Lean interactions.

How the Paper Positions Itself

The paper positions itself at the intersection of two emerging trends that it aims to unify:

Agent-based interaction with formal environments. The trend from step-level provers (high interaction frequency, low per-step complexity) and whole-proof provers (low interaction frequency, high per-generation complexity) toward an intermediate paradigm where the model dynamically controls its interaction granularity. The paper argues this is the "superior paradigm in terms of both capability and efficiency" (Section 3.1), and provides the first large-scale RL demonstration of this claim.
Leveraging natural-language reasoning to accelerate formal proving. Rather than treating natural-language proving as a competitor to formal proving (the framing that motivates the paper's opening question), the paper treats it as a complement. The sketch model explicitly uses the capabilities of a strong natural-language prover (initialized from Doubao-Seed-1.6) to generate proof plans that the formal prover can then execute. This reverses the usual direction of formalization: instead of translating an informal proof token-by-token into formal syntax, the system abstracts the proof into a lemma structure and delegates low-level formal details to the agentic prover.

The paper explicitly contrasts its sketch-based approach with Hilbert [22], which also uses a general reasoning model for informal proving and a specialized Lean model for verification. The key difference is that Hilbert feeds the natural-language proof directly to the formal prover, whereas Seed-Prover 1.5 interposes a trained sketch model that transforms the natural-language proof into a structured formal decomposition. This is a learned interface, not a hand-crafted prompt, and the rubric RL training ensures it produces decompositions that are both structurally sound (verified by Lean) and semantically useful (verified by the LLM judge).

The paper's title — "Mastering Undergraduate-Level Theorem Proving via Learning from Experience" — encapsulates its thesis. The emphasis is on learning from experience: the agentic prover learns optimal interaction patterns through thousands of Lean interactions during RL training; the sketch model learns effective decomposition strategies through rubric-based feedback; and the test-time workflow learns (implicitly) through recursive decomposition and retry loops. This is positioned as a contrast both to systems that rely primarily on expensive search at test time (AlphaProof's 500 TPU-days per problem) and to systems that are trained once via SFT without continued experiential learning (Seed-Prover 1.0's medium workflow).

3. Technical Approach

3.1 Reader Orientation

Seed-Prover 1.5 is a two-model system that proves mathematical theorems in the Lean 4 formal verification language: an agentic prover (trained via large-scale RL to interact dynamically with Lean, a math library search tool, and a Python executor) and a sketch model (trained via rubric-based RL to translate natural-language proofs into structured Lean lemma decompositions). The system solves the problem of formal theorem proving being vastly more expensive than natural-language reasoning by introducing a hierarchical test-time workflow where the sketch model decomposes complex theorems into simpler sub-goals, and the agentic prover — operating at the granularity of lemmas rather than individual tactics or whole proofs — incrementally constructs and caches verified proof steps, learning from both its training experience and its runtime interactions with the Lean environment.

3.2 Big-Picture Architecture (Diagram in Words)

The system consists of five interconnected components:

Natural Language Prover — An LLM (initialized from Doubao-Seed-1.6) that generates rigorous, lemma-style natural-language proofs from formal Lean statements. It serves as the initial reasoning engine, producing high-level proof strategies that the rest of the system will formalize.
Sketch Model — A VAPO-trained translation model that converts natural-language proofs into Lean sketches: structured decompositions containing a main_proof body and multiple lemma statements (initially admitted with sorry). It acts as the bridge between informal reasoning and formal syntax.
Agentic Lean Prover — A tool-integrated RL-trained model that interacts with Lean via lemma-level verification, with mathlib for semantic theorem search, and with a Python executor for computational experiments. It is the workhorse that discharges individual lemmas by constructing and verifying formal proofs.
Lean REPL Environment (LooKeng) — A Python interface to the Lean 4 compiler that accepts code submissions, returns structured feedback (compilation errors, goal states), and maintains a cached context of previously verified lemmas. It serves as the ground-truth verifier.
Test-Time Orchestration — A hierarchical search procedure that recursively applies the pipeline: the Natural Language Prover generates a proof, the Sketch Model decomposes it into lemmas, the Agentic Prover attempts to prove each lemma, and if any lemma fails, the system recursively re-decomposes. Failed lemmas trigger sketch refinement; successful lemmas are cached and assembled into the final proof.

Information flow at inference time: A formal Lean statement enters the system → the Natural Language Prover produces a lemma-style natural-language proof → the Sketch Model translates this into a Lean sketch with N independent lemma sub-goals → the agentic prover attempts each lemma under a compute budget of Pass@3×3 → if a lemma cannot be proved, the system recursively applies the natural-language→sketch decomposition to that lemma → once all leaf-node lemmas are proved, they are assembled into the complete formal proof.

3.3 Roadmap for the Deep Dive

First, the agentic prover's inference mechanism and tool ecosystem (Section 3.1), because the agent's dynamic interaction loop — how it calls Lean, searches mathlib, and executes Python — defines the core capability that RL training then optimizes. Understanding the tools and the interaction protocol is prerequisite to understanding what RL is optimizing.
Second, the post-training pipeline (Section 3.2), covering the cold-start SFT data construction, the RL dataset curation strategy (filtering out provable examples to focus on challenging instances), and the VAPO training algorithm with outcome-based rewards. This is where the agent learns how to use the tools effectively, and the training dynamics (Figure 3, Figure 4) reveal the behavioral changes RL induces.
Third, the sketch model (Section 3.3), since it operates on a different axis — decomposition rather than execution — and requires a fundamentally different reward mechanism (rubric-based LLM evaluation rather than Lean verification). Understanding the rubric design and the binary reward function (Equation 2) is essential for understanding why the sketch model produces useful decompositions.
Fourth, the test-time workflow (Section 3.4), which orchestrates the three specialized agents (Natural Language Prover, Sketch Model, Agentic Prover) in a recursive decomposition loop. This is where the separate components are integrated into a complete system, and the scaling behavior (Figure 6) reveals how increasing compute budget improves solve rates.

3.4 Detailed, Sentence-Based Technical Breakdown

This is primarily a systems and RL training paper whose core idea is that a formal theorem prover can achieve substantial capability gains by learning from extensive interaction with the Lean environment — both through agentic RL training on tool use and through rubric-guided learning of proof decomposition — rather than relying on monolithic single-pass generation or expensive post-hoc search.

Agentic Prover: Inference Mechanism and Tool Ecosystem

The agentic prover is the core proof-construction engine. Unlike prior step-level provers that generate one Lean tactic at a time, or whole-proof provers that generate an entire proof in one shot, the agentic prover operates at the granularity of lemmas — semi-autonomous sub-proofs that are independently verified, cached, and composed into larger arguments. This design choice is motivated by the observation that human mathematicians interact with proof assistants at precisely this intermediate granularity: they prove useful intermediate facts, verify they compile, and use them as building blocks.

The interaction loop. Figure 7 (referenced in Section 3.1 as illustrating the inference workflow, though the text notes a discrepancy — the figure is labeled Figure 2 in the paper's cross-reference and Figure 7 in the text; we follow the text's reference to Figure 7) depicts a multi-turn trajectory where the model alternates between natural-language reasoning and tool invocations. Each turn proceeds as follows:

The model receives the current Lean context (the original formal statement plus all previously verified lemmas, which have been converted to axiom declarations for reuse).
The model generates natural-language reasoning about what remains to be proved and what strategy to pursue.
When the model decides to take action, it emits a structured tool call — for example, invoking verify_lean to compile a lemma, mathlib_semantic_search to find relevant theorems, or executing Python for numerical experiments.
The tool response (compilation feedback, search results, computation output) is appended to the conversation.
The model processes the feedback and either continues reasoning, invokes additional tools, or finalizes the proof.

Termination conditions. Generation terminates when either (a) the final theorem is successfully verified by the Lean compiler, or (b) the interaction budget is exhausted — a maximum sequence length of 64K tokens and a limit of 28 tool calls. If the budget is exhausted without success, the system can apply the light inference strategy from Seed-Prover 1.0 [3], where the model performs self-summarization over the failed trajectory and initiates a new trajectory conditioned on that summary. For evaluation purposes, a single trajectory (with or without summarization-based retries under the light inference setting) constitutes one Pass@1 attempt.

Incremental lemma caching. The mechanism that distinguishes this agentic prover from both step-level and whole-proof approaches is its incremental caching strategy. When a lemma is successfully verified by the Lean compiler (the verify_lean tool returns with "No goals"), the lemma is saved to the running context and converted to an axiom declaration. This means subsequent reasoning steps can directly reference the lemma by name without re-proving it, and the context window contains only the statements of proved lemmas rather than their full proof code. The paper argues this provides three concrete advantages over whole-proof generation:

Decomposition of complexity: The model can focus on resolving the immediate sub-goal without needing to maintain a global proof plan in its context. Each lemma is an isolated proving task, reducing the cognitive burden on the model.
Context efficiency: By caching only lemma statements (not full proofs), the context overhead grows linearly with the number of proved lemmas rather than quadratically with proof length. This is particularly important given the 64K token budget — a 5000-token proof body would consume nearly 8% of the budget if stored in full, and multiple such proofs would quickly exhaust the window.
Flexible inference control: The cached lemma structure enables strategies that would be impossible with whole-proof generation. For example, the system can prune irrelevant intermediate steps, backtrack to restart the conversation at specific points, or reuse lemmas across multiple proof attempts without regenerating them.

The tools. The agentic prover has access to three categories of tools, all integrated through a unified function-calling interface:

1. Lean verification (verify_lean). This tool submits Lean code to the LooKeng [3] REPL4-based Python interface, which compiles it against Lean 4 and returns structured feedback. The key design choice is that the model submits individual lemmas rather than entire proofs at each call. The lemma header (the statement being proved) is added to the running context; if the proof compiles successfully, the lemma is cached. If compilation fails, the tool returns structured error information — the specific line where the error occurred, the severity level, and a message describing the problem (e.g., "unsolved goals: ... ⊢ H = ⊤"). This granular feedback enables the model to diagnose and correct errors locally, without regenerating the entire proof.

2. Mathlib search (mathlib_semantic_search). This tool performs embedding-based retrieval against a fixed commit of mathlib4 (v4.22.0) to find theorems, lemmas, or definitions semantically related to a natural-language query. The model provides a query string (e.g., "If a subgroup has finite index in an additive group, then there..."), and the tool returns the most relevant declarations with their signatures, file locations, and semantic descriptions. Crucially, the paper notes that during inference, the model adapts its search behavior to the problem domain: on Fate-H (which relies heavily on mathlib knowledge), the model averaged approximately 10 search calls per trajectory, whereas on PutnamBench it averaged only 1–2. This adaptive behavior emerged from RL training rather than being explicitly programmed, and the number of search calls decreased in later checkpoints while performance improved (Figure 5), suggesting the model internalizes knowledge from search results over the course of training — it learns which theorems to call directly without searching.

3. Python execution. The model can generate and execute Python scripts for numerical experiments, computational checks, and other auxiliary computations within the proving trajectory. This is a lightweight computational capability that complements the formal reasoning — for example, verifying a numerical conjecture before attempting a formal proof, or computing specific values that inform a proof strategy.

Why lemma granularity over alternatives. The paper's core design argument is that lemma-level interaction hits a "sweet spot" between the extremes of step-level and whole-proof interaction. Step-level provers interact too frequently: each rw, apply, or simp command triggers a separate API call, meaning the model must maintain coherence across hundreds of round-trips for a single proof, and the context window accumulates tactical detail that is irrelevant for higher-level reasoning. Whole-proof provers interact too infrequently: they receive a single pass/fail verdict with error messages that may be far removed from their root cause, and they cannot recover from mid-proof errors without regenerating the entire proof from scratch. Lemma-level interaction provides balanced feedback: the model receives verification after each sub-goal is attempted, can cache successes, and can decompose a complex proof into manageable chunks where each chunk is large enough to avoid interaction overhead but small enough that errors can be localized.

The "conversion to axiom" detail. A subtle but important technical point: when a lemma is successfully verified, it is not merely saved as a proved theorem — it is converted to an axiom declaration in the running context. This means the model can use the lemma's statement without carrying its proof body in the context window. This is semantically sound because a verified lemma is logically true; treating it as an axiom for subsequent reasoning does not compromise correctness. However, it is a pragmatic choice that prioritizes context efficiency over formal elegance — a choice that proves essential given the 64K token budget constraint.

Post-Training Pipeline: From SFT Cold Start to VAPO Reinforcement Learning

The agentic prover is not trained from scratch. It is post-trained from the Seed-Prover 1.0 model [3] through a two-stage process: supervised fine-tuning (cold start) followed by VAPO-based reinforcement learning.

Cold start via supervised fine-tuning. To transition the base Seed-Prover 1.0 model into an agentic tool-use model, the authors construct in-house synthetic training data that demonstrates the desired interaction patterns. This SFT data teaches the model the specific tool invocation syntax, the expected sequence of reasoning-then-action, and the conventions of the Lean proving environment. The data is not described in detail — the paper states only that it is "in-house synthetic training data" used to "enable the model to learn our tool invocation patterns and interactions specific to the proving environment." This is a standard approach for bootstrapping tool-use capabilities: the SFT stage provides the model with a basic competency in the interaction protocol, which RL then optimizes for effectiveness and efficiency.

RL training dataset construction. The RL training set is constructed from a mixture of publicly available datasets [2, 11, 16, 23, 29] and in-house formalized math textbooks, including Graduate Texts in Mathematics. However, not all available problems are used directly. The authors apply a sophisticated filtering procedure designed to focus RL training on challenging but provable instances:

Initial evaluation: The SFT model is evaluated on each candidate problem under a light inference setting (Pass@4×8). In this setting, if a trajectory fails to complete a proof, the model performs self-summarization over the failed attempt and initiates a new trajectory conditioned on the summary, with up to 4 independent trajectories each allowed 8 summarization-based retries.
Exclusion of already-solved problems: Any problem that the SFT model successfully proves more than three times under this setting is excluded. The rationale is that RL training provides minimal learning signal on problems the model already handles reliably; computational resources are better spent on problems where improvement is possible.
Exclusion of unprovable problems: Any problem that the SFT model cannot prove under any prompting strategy (direct proving, natural-language-conditioned proving, or summarization-conditioned proving) is removed. RL requires eventual positive reward to learn from; if a problem is fundamentally beyond the model's current capability regardless of context, it provides only negative feedback and does not support credit assignment.
Retention of context-dependent problems: A crucial nuance: if a formal statement is provable when conditioned on a summarization prompt but not under the direct proving prompt, the example is retained under the direct proving prompt. This is because the statement is provable in principle (the model can reach it with additional context), and RL training might improve the model's efficiency so that it can prove it directly without needing summarization. This creates a curriculum where the model learns to internalize the strategies that previously required external scaffolding.

RL algorithm: VAPO with tool integration. Reinforcement learning is implemented using VAPO [31] (Value-based Actor-critic with Proximal Policy Optimization), adapted following the ReTool [4] approach to enable tool-integrated RL — that is, the policy generates interleaved text and tool calls, the environment executes the tool calls and returns results, and the advantage estimation accounts for the full multi-turn trajectory.

The reward function is simple and grounded entirely in formal verification:

$R = \begin{cases} +1 & \text{if a valid proof is completed and verified by the Lean compiler} \\ -1 & \text{otherwise} \end{cases}$

where the reward is binary: the model receives +1 for successfully compiling a complete proof of the target theorem, and −1 for any other outcome (timeout, compilation error, budget exhaustion).

What it computes: a single scalar signal per trajectory indicating whether the proof succeeded. There is no partial credit, no step-level shaping, and no intermediate reward — the model only learns from the terminal outcome.

Why this form: the Lean compiler provides an objective, non-gameable verification signal. Outcome-based rewards avoid the reward engineering challenges of designing intermediate sub-goal rewards (which might inadvertently incentivize the model to game the sub-goal signal rather than completing proofs), and they align naturally with the binary nature of formal verification (compiles or doesn't). The symmetry of +1/−1 (rather than, say, +1/0) provides a gradient signal even on failure: negative reward penalizes trajectories that waste budget, encouraging the model to learn efficient tool use and avoid dead-end reasoning paths.

The RL objective follows a clipped PPO variant:

$L^{\text{PPO}}(\theta) = -\frac{1}{G \sum_{i=1}^G |o_i|} \sum_{i=1}^G \sum_{t=1}^{|o_i|} \min\left( r_{i,t}(\theta) \hat{A}_{i,t}, \ \text{clip}\left(r_{i,t}(\theta), 1 - \varepsilon_{\text{low}}, 1 + \varepsilon_{\text{high}}\right) \hat{A}_{i,t} \right)$

where $G$ is the training batch size (the number of trajectories in a batch), $o_i$ is the $i$ -th trajectory (a sequence of interleaved text tokens and tool responses), $|o_i|$ is its length in tokens, $\hat{A}_{i,t}$ is the estimated advantage at timestep $t$ , and $\varepsilon_{\text{low}}, \varepsilon_{\text{high}}$ are asymmetric clipping hyperparameters. The probability ratio $r_{i,t}(\theta) = \frac{\pi_\theta(a_t|s_t; \mathcal{T})}{\pi_{\theta_{\text{old}}}(a_t|s_t; \mathcal{T})}$ compares the current policy's probability of generating action $a_t$ given state $s_t$ and tool context $\mathcal{T}$ against the old policy's probability (frozen during the current PPO epoch).

What it computes: the standard PPO clipped surrogate objective, applied to multi-turn tool-use trajectories. For each token in each trajectory, the objective encourages increasing the probability of actions that had positive advantage (were better than expected) and decreasing the probability of actions with negative advantage, subject to clipping that prevents the policy from changing too drastically in any single update.

Why this form: VAPO extends standard PPO with modifications for reasoning tasks (the paper cites VAPO [31] for the specific algorithm, but the clipped objective is presented as Equation 1). The asymmetric clipping ( $\varepsilon_{\text{low}}$ and $\varepsilon_{\text{high}}$ are distinct) allows the algorithm to be more conservative when decreasing probabilities than when increasing them, or vice versa — a common technique in reasoning-oriented RL where over-optimistic policy updates can cause collapse. The tool context $\mathcal{T}$ in the probability ratio acknowledges that the policy conditions on the full history of tool interactions, not just the raw text.

Training dynamics and behavioral changes. The paper tracks several metrics across 1200 RL training steps, revealing systematic behavioral changes:

Training accuracy (Figure 3a): The moving average of batch-level accuracy increases from approximately 50% at initialization to nearly 90% after 1000+ steps. This monotonic improvement suggests that the model is genuinely learning from the environment feedback rather than saturating early.
Efficiency improvements (Figure 4a, 4b): The average number of function calls per trajectory drops from approximately 15 to 10, and the average total sequence length decreases from approximately 28,000 to 17,000 tokens. This is evidence that the model is learning to use tools more strategically — avoiding redundant or "trial-and-error" invocations that consume budget without advancing the proof.
Long-horizon reasoning (Figure 4c, 4d): For samples with longer response lengths (16K–32K and 32K–64K tokens), the model's average score (a proxy for proof success) improves over training steps. This indicates improved capability on complex, long-horizon problems. However, scores in the 32K–64K range remain lower and more variable, suggesting that effectively reasoning over extremely long contexts remains an open challenge.
Search behavior adaptation (Figure 5): The number of search tool calls decreases in later checkpoints while performance continues to improve. On PutnamBench, the proportion of proved samples using ≤10 search calls increases from 71.1% to 79.7% between the 495th and 1055th step checkpoints. On Fate-H, the proportion of proved samples using >20 search calls drops from 53.7% to 45.6%. The paper interprets this as the model "internalizing knowledge from search results" — early training teaches the model which theorems exist and are useful, and later training enables the model to retrieve this knowledge directly from its parameters rather than through explicit search calls.

Test-set evaluation protocol. For evaluation, the authors select the best-performing checkpoint (at the 1055th training step) and evaluate using two settings: direct solving (Pass@8×1 — eight independent trajectories, each a single attempt without summarization) and light inference (Pass@8×8 — eight independent trajectories, each with up to 8 summarization-based retries). The results in Table 1 compare this against Seed-Prover 1.0's medium workflow, which consumed 18 H20-days per problem. The agentic prover under Pass@8×8 solves 359/660 on PutnamBench versus 331/660 for the 1.0 medium workflow, and 57/100 on Fate-H versus 35/100 — substantial improvements despite the agentic prover using the lighter Pass@8×8 budget compared to the 1.0 medium workflow's more expensive resource allocation. On Fate-X, the improvement is modest (10/100 versus 9/100), reflecting the fundamental difficulty of PhD-level problems that exceed current Mathlib coverage and require knowledge beyond the training distribution.

Sketch Model: Rubric-Guided Decomposition from Natural Language to Lean

The sketch model addresses a problem the agentic prover cannot solve on its own: for complex theorems, the proof is too long and intricate to construct monolithically. A human mathematician would not attempt to prove a 1000-line theorem in a single pass; they would first outline a proof strategy, identify key lemmas, and then prove each lemma independently. The sketch model automates this decomposition step, translating a natural-language proof into a structured Lean plan.

What the sketch model produces. Given a formal Lean statement and its natural-language proof, the sketch model generates a lemma-style Lean sketch: a Lean file containing:

A set of lemma declarations, each stating an intermediate mathematical fact that is useful for the main proof. These lemmas are initially admitted with sorry (Lean's placeholder for an unproven statement).
A main_proof body that demonstrates how these lemmas logically combine to prove the original theorem. Critically, the main proof body must explicitly show the assembly logic — using have, apply, constructor, intro, and other standard tactics to orchestrate the lemmas — rather than delegating the assembly to an opaque wrapper lemma (which would constitute "proof by delegation" and invalidate the sketch).

The sketch model is not proving anything itself; it is producing a proof plan whose quality is evaluated along two dimensions: (1) structural soundness (does the Lean code type-check modulo the sorry-filled lemmas?), and (2) semantic utility (are the lemmas mathematically valid, sufficiently decomposed, and genuinely easier than the original problem?).

Training the sketch model with rubric-based RL. Training this model requires a reward signal that captures both structural and semantic quality. Structural soundness can be verified by the Lean compiler directly (a sketch with minor errors beyond the sorry-admitted lemmas will fail to compile), but semantic utility requires a more nuanced evaluator. The paper's solution is rubric reinforcement learning: using an LLM-as-a-Judge with a structured evaluation rubric to produce a binary reward signal that drives VAPO training.

The reward function fuses Lean verification and natural-language quality assessment:

$R = \begin{cases} 1 & \text{if } N_{\text{lemmas}} \geq 3 \land S_{\text{FL}} \geq 0 \land S_{\text{NL}} \geq 0.7, \\ -1 & \text{otherwise.} \end{cases}$

where $N_{\text{lemmas}}$ is the number of generated lemmas in the sketch, $S_{\text{FL}}$ is the Lean verification score (indicating structural correctness), and $S_{\text{NL}}$ is the natural language quality score produced by the rubric-based evaluator.

What it computes: a binary reward (+1 for a good sketch, −1 otherwise) determined by three thresholds. The sketch must (1) contain at least 3 lemmas to qualify as sufficient decomposition, (2) pass Lean's structural checks ( $S_{\text{FL}} \geq 0$ means the code compiles except for the sorry-admitted lemma proofs), and (3) achieve a natural language quality score of at least $0.7$ , indicating that an LLM judge using a structured rubric deems the lemmas mathematically valid, well-aligned with the natural-language proof, and genuinely decompositional (each lemma is strictly easier than the original theorem).

Why this form: each threshold encodes a necessary condition for sketch quality. $N_{\text{lemmas}} \geq 3$ is a hard constraint against trivial decomposition (breaking a theorem into one or two lemmas that are essentially restatements of the original goal — a degenerate sketch that doesn't simplify the problem). $S_{\text{FL}} \geq 0$ is a structural sanity check: if the sketch itself doesn't compile (e.g., the lemma statements are ill-typed), it cannot guide the agentic prover regardless of semantic quality. $S_{\text{NL}} \geq 0.7$ provides a calibrated semantic gate: the rubric evaluator must be reasonably confident that the lemmas are correct (not mathematically false) and useful (not trivial or circular). The conjunctive form means the sketch must satisfy all three criteria — a single failure produces −1, creating a strong incentive for the model to produce sketches that are simultaneously structurally sound and semantically meaningful. The +1/-1 binary structure (rather than a continuous quality score) follows the same outcome-based RL philosophy as the agentic prover: the model learns to produce sketches that pass the quality bar, not to game a continuous metric.

The rubric evaluation pipeline (from Appendix B). The $S_{\text{NL}}$ score is not produced by a simple scalar reward model — it is the output of a sophisticated LLM-as-a-Judge process that the paper describes through two detailed prompts (Prompt 1: Atomic Lemma Verification, and Prompt 2: Proof Strategy Alignment, in Appendix B). The evaluation proceeds in two phases:

Phase 1: Lemma verification. Each lemma in the sketch is independently evaluated for mathematical correctness. The evaluator (an LLM prompted as a "rigorous mathematician and an expert Lean 4 formalization engineer") checks whether the lemma statement is provable from standard mathematical axioms, treating the sketch's other lemmas and the main theorem body as untrusted (they may be hallucinated or incorrect). The evaluator is explicitly instructed to:

Resolve custom definitions by consulting the sketch, but ignore all other lemma/theorem entries.
Attempt to construct a proof or find a counter-example.
Check for missing hypotheses that would cause junk-value failures in Lean 4 (e.g., missing Summable hypotheses causing infinite sums to evaluate to 0, missing IntegrableOn hypotheses causing integrals to be undefined on non-compact domains).
Apply rigorous junk value analysis: if a statement holds in standard mathematics but fails in Lean because of the specific way Lean defines edge cases (e.g., 1/0 = 0, Real.sqrt (-1) = 0, divergent infinite sums equal 0), the lemma is marked as incorrect.

If any lemma is found to be mathematically invalid, the sketch is immediately rejected ( $S_{\text{NL}} = -1$ ). The paper notes that "using the natural language prover to disprove is cheaper than using a theorem prover" — an important practical consideration: formal counterexample finding is expensive; LLM-based semantic evaluation is cheaper and catches most invalid lemmas.

Phase 2: Proof strategy alignment (for sketches that pass Phase 1). The evaluator assesses the overall sketch quality using a structured rubric with two major dimensions:

Structural alignment (50% weight): How well does the sketch's lemma structure align with an optimal decomposition derived from the natural-language proof? The rubric defines two quality tiers: Tier 1 (strategic decomposition) — the sketch correctly breaks the problem into its main logical parts but doesn't create deeper, search-simplifying lemmas; Tier 2 (search simplification) — the sketch identifies and lemmatizes core mathematical steps that make the problem easier to search, closely mirroring an ideal proof plan.
Lemma value (50% weight): Are the individual lemmas high-quality for search-based solving? This rewards lemmas that are self-contained (carrying all necessary context, not relying on local variables from the main proof), that isolate concrete solvable sub-problems, and that effectively absorb the "essence" of the natural-language proof steps.

The scoring also incorporates a veto mechanism that rejects sketches with fatal flaws regardless of other qualities. Three veto triggers are defined:

Fatal misalignment: The sketch's core strategy (e.g., induction on n) completely contradicts the natural-language proof's stated strategy (e.g., casework on x). This means the sketch is solving a different problem or using an incompatible approach.
Proof by delegation: The main theorem body is "hollow" — it delegates the assembly logic to a wrapper lemma that shares the same goal as the main theorem, hiding the reasoning in an opaque sorry. The evaluation prompt distinguishes this from valid assembly patterns where the main proof body explicitly shows how lemmas are combined using standard tactics.
Invalid lemma: Any lemma is (a) mathematically false/unprovable, (b) missing context/not self-contained, (c) trivial (offering no simplification — e.g., a simple logical tautology or direct application of a hypothesis), (d) circular (restating the original goal without simplification), or (e) invalid due to Lean junk value semantics.

For sketches that pass the veto checks, the final score is computed as a weighted combination with a utilization penalty:

$\text{final\_score} = \text{round}\left( (0.4 \times \text{alignment} + 0.6 \times \text{value}) \times \frac{\text{lemmas\_used\_in\_main\_proof}}{\text{total\_valid\_lemmas}}, 1 \right)$

where alignment and value are scores from 0–10, and the utilization factor penalizes sketches that propose valid lemmas but don't actually use them in the main proof body. This incentivizes the model to produce sketches where every lemma serves a purpose.

Why rubric-based evaluation over scalar reward models. The paper argues, through the rubric design, that rubric-based LLM-as-a-Judge evaluation achieves "better generalization than scalar-based models" (Section 3.3). The mechanism is the rubric's structural decomposition: by breaking evaluation into explicit dimensions (alignment, value, utilization), defining concrete veto triggers, and requiring the evaluator to construct an ideal decomposition rubric for comparison, the evaluation escapes the "single number" limitation of scalar reward models. A scalar model might assign a moderate score to a sketch that looks superficially plausible but contains a fatal lemma error; the rubric's hard veto catches this. A scalar model might penalize a sketch for being "too simple" without recognizing that the simplicity is appropriate for straightforward problems; the rubric's tier system (Tier 1 vs. Tier 2) contextualizes scores based on what decomposition is appropriate for the problem's complexity.

Training the sketch model with VAPO. Once the rubric pipeline produces binary rewards (the final_score is thresholded at 0.7 as specified in Equation 2's $S_{\text{NL}} \geq 0.7$ condition), the sketch model is optimized using VAPO with the same clipped surrogate objective structure as the agentic prover (Equation 1). The key difference is in the reward source: the agentic prover receives rewards from Lean verification directly; the sketch model receives rewards from the rubric pipeline, which is itself a learned evaluator (an LLM with carefully crafted prompts). This creates an interesting training dynamic: the sketch model is learning from a proxy reward signal that approximates true sketch quality, and the quality of this proxy depends on the rubric prompt's design. The paper's detailed prompt engineering (12+ pages of Appendix B) reflects the effort required to make this proxy reliable enough to serve as an RL reward.

Why the sketch model is necessary (rather than having the agentic prover decompose proofs itself). The paper's architecture separates decomposition (sketch model) from execution (agentic prover) for two reasons:

Specialization: Decomposition requires understanding the high-level mathematical structure and aligning with natural-language proofs — skills that benefit from the broad pre-training of a general-purpose reasoning model (Doubao-Seed-1.6). Execution requires detailed knowledge of Lean syntax, mathlib theorems, and tool-use strategies — skills that benefit from specialized RL in the Lean environment. Separating these roles allows each model to be optimized for its task without interference.
Parallelization at test time: Once the sketch decomposes a theorem into N lemmas, the agentic prover can attempt to prove those lemmas in parallel (under the Pass@3×3 budget per lemma). This transforms a single long-horizon proof problem into N independent sub-problems that can be solved concurrently, dramatically reducing wall-clock time. If the agentic prover were responsible for both decomposition and execution, it would need to sequentially decompose and then prove — a slower process.

Test-Time Workflow: Hierarchical Multi-Agent Collaboration

The full Seed-Prover 1.5 system operates not as a single model but as an orchestrated collaboration between three specialized agents, arranged in a recursive decomposition loop.

The three agents and their roles:

Natural Language Prover: An LLM initialized from Doubao-Seed-1.6, optimized for generating rigorous natural-language proofs. Its role is purely generative: given a formal Lean statement, it produces a lemma-style natural-language proof. This agent does not interact with Lean or tools — it is a straightforward text-to-text model operating in natural language.
Sketch Model: The rubric-RL-trained model described in Section 3.3. It takes the formal statement and the natural-language proof as input, and produces a lemma-style Lean sketch (structured decomposition with N lemmas and a main_proof body). This agent bridges the natural-language reasoning and formal syntax.
Agentic Lean Prover: The VAPO-RL-trained model described in Section 3.1 and 3.2. It takes individual lemma statements as input and attempts to construct verified Lean proofs using its tool ecosystem (Lean verification, mathlib search, Python execution). This is the only agent that produces verified formal proofs.

The recursive decomposition loop. The workflow for a given formal statement proceeds as follows (Section 3.4):

Step 1 — Natural-language proof generation. The Natural Language Prover receives the formal Lean statement and generates a natural-language proof. The paper does not specify the exact prompt format, but notes that the natural-language prover is "optimized for natural language proving" and produces "rigorous, lemma-style natural language proofs" — meaning the proof itself is structured into lemmas and sub-goals, not just a prose narrative.

Step 2 — Sketch decomposition. The Sketch Model receives the formal statement and the natural-language proof, and produces a Lean sketch with N lemmas. These lemmas are initially unproven (sorry), but the sketch has been verified to be structurally sound (by Lean) and semantically useful (by the rubric evaluator during training, though this evaluation is not repeated at test time — the sketch model's generation is used directly).

Step 3 — Lemma proving. For each unsolved lemma in the sketch, the Agentic Lean Prover attempts to prove or disprove it, operating under a compute budget of Pass@3×3: three independent trajectories, each with up to three summarization-based retries following the light inference protocol. This means each lemma receives up to 9 total proof attempts.

Step 4 — Recursive decomposition for failed lemmas. If the agentic prover cannot find a proof for a lemma within its budget, the system recursively applies the pipeline to that lemma: the Natural Language Prover generates a natural-language proof of the lemma, the Sketch Model decomposes it into sub-lemmas, and the Agentic Prover attempts those sub-lemmas. This recursion can proceed up to the maximum search depth.

Step 5 — Disproof handling. If a lemma is disproved (the agentic prover finds a counterexample showing the lemma is false), the system reverts to the Sketch Model to refine the original sketch. The paper does not specify the refinement mechanism in detail, but the implication is that a disproved lemma indicates a flaw in the natural-language proof or its translation, requiring the sketch to be restructured with different lemmas.

Step 6 — Termination. The process repeats until either (a) every leaf node in the decomposition tree is successfully proved by the Lean Prover (at which point the proofs are assembled into a complete formal proof of the original theorem), or (b) the maximum search depth is reached without resolution.

Maximum search depth and restart mechanism. For the PutnamBench evaluation (Section 4.2), the system is configured with an initial maximum search depth of 4. If a problem reaches this limit without resolution, the system incorporates all lemmas successfully proved during the search into the context and restarts the search from scratch. This effectively extends the maximum search depth to 8 for each problem — the initial 4-level search, followed by a second 4-level search that builds on the partial results from the first attempt. This restart mechanism is significant because it converts partial progress (lemmas proved in the first attempt) into permanent context that the second attempt can leverage, potentially enabling proofs that were out of reach in a single pass.

Pass@k×m budget notation. The paper consistently uses the notation Pass@k×m to specify inference compute budgets. This means: k independent trajectories (fresh conversations with the agentic prover), each trajectory allowed up to m summarization-based retries under the light inference protocol. A trajectory that succeeds on its first attempt consumes only 1 of its m retry budget; a trajectory that fails exhausts all m retries. The Pass@k×m budget is the total number of proof attempts across all trajectories and retries — $k \times m$ maximum total attempts per problem, assuming all trajectories exhaust their retry budgets. In practice, many trajectories succeed early, so the actual compute consumed is lower than the budget.

Why this workflow structure over monolithic proving. The hierarchical workflow provides two key advantages that neither the agentic prover alone nor the sketch model alone could achieve:

Computational tractability for long proofs: Complex theorems in Lean can require thousands of lines of code. A monolithic single-pass generation (even with the agentic prover's lemma caching) would need to maintain coherence across a 64K+ context window, which the training dynamics in Figure 4d suggest remains challenging. Decomposition breaks the problem into sub-proofs that are individually within the model's effective context range.
Graceful degradation on hard problems: If a lemma cannot be proved, the system doesn't fail entirely — it recursively decomposes that lemma, potentially finding a proof strategy that operates at a finer granularity. If a lemma is disproved, the system learns that the current decomposition is flawed and can attempt an alternative. This contrasts with whole-proof approaches where a single failure is terminal.

Compute budget measurement. The paper measures test-time compute in H20-days per problem, where an H20-day represents 24 hours of computation on an H20 GPU. For the PutnamBench evaluation, Seed-Prover 1.5 uses a budget of 10 H20-days per problem (Table 2), substantially less than Seed-Prover 1.0's medium workflow (18 H20-days per problem) and orders of magnitude less than AlphaProof's 500 TPU-days per problem. For the Putnam 2025 evaluation, a maximum budget of 40 H20-days per problem was allocated, but all 11 solved problems were completed within 9 hours of wall-clock time (Table 4) — the budget was not fully consumed because the parallel decomposition allowed rapid solving.

Scaling behavior (Figure 6). The test-time scaling analysis on PutnamBench shows two patterns:

Log-linear scaling with compute (Figure 6a): The number of solved problems increases log-linearly with computational budget. Doubling the compute budget (measured in H20-days per problem) produces a roughly constant increment in the number of solved problems. This is characteristic of systems where additional compute enables exploration of increasingly difficult problem instances — each additional unit of compute has diminishing but non-zero returns.
Heavy-tailed solve time distribution (Figure 6b): A histogram of solve times shows that the majority of problems are solved within the first few hours, but a long tail of more challenging problems is discovered as search continues up to the 53rd hour. This suggests that the test-time workflow is effective at rapidly solving most problems within its capability range, with the remaining compute budget spent on a small number of genuinely hard instances that require deep recursive decomposition.

4. Key Insights and Innovations

Innovation 1: Agentic Reinforcement Learning as a Third Interaction Paradigm for Formal Theorem Proving

The paper's most fundamental conceptual move is redefining how an LLM should interact with a proof assistant — not at the granularity of individual tactics (step-level), not at the granularity of complete proofs (whole-proof), but at the dynamically chosen granularity of lemmas and sub-goals, learned through experience rather than prescribed by architecture. This is not merely a new system design; it is a diagnosis that the field has been stuck in an inefficient dichotomy, and that escaping it requires the model to learn its own interaction strategy through reinforcement learning in the Lean environment.

What the dominant paradigm was. Prior to this work, LLM-based formal provers fell cleanly into two camps. Step-level provers — Aristotle [1], AlphaProof [8], InternLM2.5-StepProver [25], BFS-Prover [27], and multi-turn off-policy RL provers [28] — generated a single Lean tactic per interaction, receiving compiler feedback after every atomic operation. This provided dense feedback but created enormous interaction overhead: a proof of moderate complexity could require hundreds of round-trips, with the context window accumulating tactical detail irrelevant to higher-level reasoning. Whole-proof provers — Seed-Prover 1.0 [3], DeepSeek-Prover-V1.5 [26] and V2 [18], Kimina-Prover [23], Goedel-Prover [12] and V2 [13], Leanabell-Prover-V2 [9] — took the opposite extreme, generating the entire proof in a single output and receiving a pass/fail verdict. This minimized interaction overhead but created a severe credit-assignment problem: error feedback arrived only after the entire proof was generated, making it difficult to localize and fix mistakes, and partially correct proofs provided no salvageable intermediate results.

The field implicitly accepted this dichotomy as exhaustive — either you interact frequently with fine-grained feedback, or you interact once with coarse feedback. The agentic prover's lemma-level interaction, coupled with incremental caching of verified lemmas, breaks this dichotomy by creating a flexible middle ground where the model controls its own granularity: it can prove a simple lemma in a single Lean call, or decompose a complex sub-goal into multiple lemmas with interleaved search and computation. The model learns when to call Lean (not after every tactic, but after each meaningful sub-goal is attempted) and when to search mathlib or run Python instead.

Why this is fundamental, not incremental. The shift from prescribed interaction frequency to learned interaction strategy is a qualitative change in the relationship between the model and the proof assistant. Step-level and whole-proof approaches both impose a fixed granularity on the model — the model must conform to the system designer's choice of interaction frequency. The agentic approach delegates this choice to the model, which learns through RL what granularity is effective for different types of problems. The evidence that this learning occurs is in Figure 4a and 4b: over the course of RL training, the average number of function calls drops from ~15 to ~10, and the average sequence length drops from ~28K to ~17K tokens, while training accuracy simultaneously rises from 50% to 90%. This is not a system designer tuning hyperparameters — this is the model discovering, through thousands of Lean interactions, that it can achieve more with less by being strategic about when to invoke tools.

The diagnostic insight about "search internalization." Perhaps the most striking evidence for learned interaction strategy is in Figure 5, which shows that the number of mathlib search calls per trajectory decreases in later RL checkpoints while performance improves. On PutnamBench, the proportion of proved samples using ≤10 search calls increases from 71.1% to 79.7% between the 495th and 1055th training step checkpoints. On Fate-H, the proportion using >20 search calls drops from 53.7% to 45.6%. The paper interprets this as the model "internalizing knowledge from search results" — early in training, the model uses search extensively to discover which theorems exist; later, it retrieves this knowledge directly from its parameters, using search only when genuinely needed. This is a non-obvious emergent behavior that no system designer programmed; it emerged because the RL objective rewards efficiency (negative reward for budget-exhausting trajectories) and the model discovered that internalization is more efficient than repeated search.

Comparison to prior agentic approaches. The paper acknowledges prior work on agentic proving — specifically StepFun-Prover Preview [19], which "generates an entire proof and repeatedly evaluates it using the Lean compiler." The distinction is crucial: StepFun-Prover's agent loop is evaluate-then-regenerate, essentially a sophisticated retry mechanism around whole-proof generation. Seed-Prover 1.5's agent loop is incrementally-construct-and-cache, where each successful sub-proof becomes a permanent building block. The caching mechanism (converting verified lemmas to axiom declarations) means that progress is cumulative within a trajectory, not all-or-nothing. This is the difference between a system that tries different complete proofs until one works (exploration over proof space) and a system that builds proofs piece by piece (construction in proof space). The former can only succeed by finding a complete proof in its generation distribution; the latter can succeed by composing partial successes into a complete proof, even if no single generation would produce the entire proof at once.

The unexplored frontier claim. The paper explicitly states that "training such an agentic prover via large-scale RL remains an underexplored frontier area" (Section 3.1). This is not merely promotional — it reflects a genuine gap. Prior RL for theorem proving (AlphaProof [8], DeepSeek-Prover-V2 [18], Kimina-Prover [23]) was applied to step-level or whole-proof models with fixed interaction patterns. Applying RL to a model that controls its own tool-use trajectory — where the action space includes decisions about which tool to call, when to call it, and what lemma to attempt — creates a fundamentally more challenging credit-assignment problem. The fact that VAPO training succeeds in this setting (reaching 90% training accuracy and transferring to held-out benchmarks) is evidence that the approach is viable, not just plausible.

Innovation 2: Rubric-Based Reinforcement Learning as a Training Methodology for Proof Decomposition

The second major intellectual move is methodological: the paper demonstrates that an LLM-as-a-Judge with a carefully engineered rubric can serve as an effective reward model for training a model to perform proof decomposition — a task where the ultimate correctness signal (a fully verified Lean proof) is unavailable during training because the decomposition only produces proof plans, not completed proofs. This is significant not for the specific rubric design (which is engineering, albeit impressive engineering) but for what it implies about the trainability of decompositional reasoning using learned evaluators.

The core training challenge. The sketch model must learn to decompose a theorem into lemmas that are (a) mathematically valid, (b) genuinely simpler than the original theorem, and (c) structured in a way that the agentic prover can actually prove. None of these properties can be directly verified by the Lean compiler: a sketch with sorry-filled lemmas compiles trivially (the sorry placeholder makes any statement "proved" from Lean's perspective), so the compiler provides no signal about whether the lemmas are true, useful, or well-structured. The standard approach in prior work — Seed-Prover 1.0 [3], DeepSeek-Prover-V2 [18] — was to use the same model for both decomposition and proving, relying on the prover's own success/failure as an implicit decomposition quality signal. This couples the two tasks: if the prover fails to prove a lemma, it's ambiguous whether the lemma was ill-chosen (decomposition failure) or the prover was insufficiently capable (proving failure). Separating the sketch model from the agentic prover — and training the sketch model with an independent quality signal — decouples these failure modes.

Why rubric-based evaluation over scalar reward models. The paper claims that rubric-based evaluation with Long Chain-of-Thought achieves "better generalization than scalar-based models" (Section 3.3). The mechanism is the rubric's structural decomposition of the evaluation task itself: rather than asking an LLM to output a single quality score (which might capture superficial features like length or formatting while missing fatal mathematical flaws), the rubric forces the evaluator to explicitly check for specific failure modes (false lemmas, missing hypotheses, junk value edge cases, proof-by-delegation, circular reasoning), construct a concrete counterexample or proof sketch for each lemma, and then synthesize these structured assessments into a final score. This is effectively using the evaluator LLM's reasoning capability as a semantic verifier — a role that is cheaper than formal verification (which would require fully proving each lemma) but more reliable than holistic scoring (which can miss subtle mathematical errors).

The detailed prompts in Appendix B (spanning ~6 pages) reveal the sophistication required: the lemma verification prompt includes specific instructions about Lean 4 junk values (e.g., (2:ℕ) - (3:ℕ) = 0, divergent infinite sums evaluating to 0, division by zero returning 0), requiring the evaluator to check for edge cases that would make a mathematically true statement false in Lean due to the language's total-function semantics. The proof strategy alignment prompt defines a veto mechanism with three concrete triggers and distinguishes between valid assembly patterns (using constructor, have, apply to orchestrate lemmas) and invalid "proof by delegation" (wrapping the assembly logic in an opaque lemma). This level of specification is what makes the evaluator reliable enough to serve as an RL reward — and it represents a significant engineering contribution that enables the entire sketch training pipeline.

The significance beyond formal proving. The rubric-based RL methodology generalizes beyond theorem proving. Any domain where the ultimate task is too expensive to evaluate directly during training — but where human (or LLM) experts can articulate evaluation criteria in a structured rubric — could potentially use this approach. Examples might include code refactoring (where the "correctness" signal is expensive end-to-end testing), legal document drafting (where correctness requires expert review), or scientific hypothesis generation (where empirical validation takes weeks). The key insight is that structured evaluation rubrics can serve as a bridge between cheap-but-unreliable scalar evaluation and expensive-but-reliable ground-truth verification, enabling RL training in regimes where neither extreme is viable.

The binary reward design choice. The paper's choice of a binary +1/−1 reward (Equation 2) rather than a continuous quality score is conceptually important. A continuous score would allow the sketch model to receive partial credit for "almost good" sketches. But it would also create an incentive for the model to produce sketches that score highly on the rubric's surface features without being genuinely useful — the classic reward hacking problem. The conjunctive binary reward (must have ≥3 lemmas AND must compile structurally AND must score ≥0.7 on semantic quality) creates a hard quality bar: the model receives no reward unless the sketch meets all three criteria simultaneously. This is a design pattern that appears throughout the paper: the agentic prover also uses a binary +1/−1 outcome-based reward. In both cases, the binary structure avoids the incentive to game a continuous metric while still providing a learning signal (negative rewards on failure still convey information about which trajectories are unproductive).

What makes this a fundamental contribution rather than an engineering trick. The field has been using RL for formal theorem proving since at least AlphaProof [8], but always with ground-truth verification as the reward (the Lean compiler's accept/reject). Extending RL to tasks where ground-truth verification is structurally unavailable — and doing so with a learned evaluator that generalizes well enough to drive meaningful improvement — opens a new class of trainable behaviors. The sketch model learns to perform a cognitive operation (hierarchical decomposition of a proof into simpler sub-proofs) that is central to mathematical reasoning but has resisted direct training because the correctness of a decomposition cannot be verified without actually carrying out the sub-proofs. The rubric-based approach solves this by using an LLM's reasoning capability as a proxy for ground-truth verification, with enough structure (veto triggers, specific edge-case checking, explicit tier definitions) to make the proxy reliable.

Innovation 3: The Empirical Discovery That RL Transforms Interaction Efficiency, Not Just Proof Success Rate

A subtle but important finding buried in the training dynamics analysis (Figures 4 and 5) is that reinforcement learning in the agentic setting produces qualitatively different behavioral changes than what prior work on RL for theorem proving has documented. Prior RL work in this domain — AlphaProof [8], DeepSeek-Prover-V2 [18], Kimina-Prover [23] — primarily reported improvements in proof success rate (the model solves more problems after RL than before). Seed-Prover 1.5 certainly shows this (Figure 3b shows accuracy on Putnam-200 improving with RL steps), but the more distinctive finding is that RL simultaneously improves efficiency: the model solves more problems while using fewer tool calls, shorter sequences, and fewer search queries.

Why this is surprising and significant. A naive expectation for RL in tool-use settings would be that the model learns to use tools more aggressively — after all, tools provide information, and more information should lead to better decisions. The opposite occurs: the model uses tools less as training progresses, while performance improves. Figure 4a shows average function calls dropping from ~15 to ~10. Figure 4b shows average sequence length dropping from ~28K to ~17K tokens. Figure 5 shows search calls decreasing while success rates increase. This is not a result of the system designer imposing efficiency constraints — the RL reward is purely outcome-based (+1 for success, −1 for failure), with no explicit efficiency penalty beyond the implicit cost of negative rewards on failed trajectories that consume budget. The efficiency improvement emerges because, in an environment where tool calls consume context budget (limited to 64K tokens and 28 tool calls), efficient trajectories are more likely to succeed — they have more remaining budget for the actual proving work.

The mechanism: learned strategic restraint. The paper's interpretation is that RL teaches the model "strategic tool use" — knowing when not to call a tool is as important as knowing when to call one. Early in training, the model engages in "redundant or 'trial-and-error' invocations" (Section 4.1), calling mathlib search for theorems it vaguely recalls, re-verifying lemmas it already proved, running Python experiments that don't inform the proof. Late in training, the model has internalized common theorem knowledge (so fewer searches are needed), has learned to trust its cached lemmas (so fewer re-verifications), and has developed better proof planning (so fewer dead-end explorations). This is fundamentally a meta-cognitive skill — the model is learning to manage its own cognitive resources (context window, tool call budget) effectively, not just learning to produce correct proofs.

The diagnostic value of this finding. This result serves as a diagnostic that the RL training is working in a deeper way than mere pattern memorization. If the model were simply memorizing proofs for specific problems in its training set, we would not expect efficiency on those problems to improve — memorized solutions would have fixed tool-call patterns. The fact that efficiency improves suggests the model is learning generalizable strategies for interacting with the proving environment: how to decompose a problem into appropriately sized lemmas, when to search versus when to recall, how to structure a proof trajectory to minimize wasted context. This is evidence that the RL signal from Lean verification — despite being sparse, binary, and delayed — carries enough information to shape complex behavioral patterns, not just to reinforce successful proof patterns.

Connection to the "search internalization" phenomenon. The efficiency improvements are most visible in the search behavior (Figure 5), which the paper frames as "internalizing knowledge from search results." This is a concrete example of a broader phenomenon: RL in information-rich environments can teach models to compress frequently accessed information into their parameters, reducing the need for explicit retrieval. This has implications beyond theorem proving — any domain where models have access to retrieval tools during training might exhibit similar internalization dynamics, potentially explaining why retrieval-augmented generation sometimes underperforms parameter-only models on frequently tested knowledge (the model learned the knowledge during training and retrieval becomes redundant overhead).

Innovation 4: Formal-Natural Language Synergy Through Learned Decomposition Rather Than Direct Translation

The paper's architecture embodies a distinctive thesis about the relationship between natural-language and formal mathematical reasoning that differs from both dominant approaches in the literature. Rather than treating natural-language proofs as competitors to formal proofs (the zero-sum framing that motivates the paper's opening question about whether formal proving is still "viable and valuable") or as direct inputs to a translator (the approach in Hilbert [22], where a general reasoning model's natural-language proof is fed directly to a formal prover), Seed-Prover 1.5 treats natural-language reasoning as a hierarchical planner whose output is transformed by a learned decomposition model into a structured formal plan that an execution-focused agent can discharge.

What's novel about this framing. The key conceptual distinction is between translation and decomposition. Translation approaches (Hilbert [22], autoformalization work [24]) attempt to map natural-language statements to formal equivalents, preserving the surface structure of the proof. This works poorly for complex proofs because the natural structure of a proof (narrative, conceptual leaps, implicit background knowledge) does not correspond cleanly to the formal structure required by Lean (explicit type-theoretic justification for every step). Decomposition, as practiced by the sketch model, does not attempt to preserve the natural-language proof's structure; it uses the natural-language proof as a semantic guide to produce a formal structure (lemmas) that is optimized for the agentic prover's capabilities, not for fidelity to the original text.

This is a subtle but important shift in how we think about the natural-to-formal interface. The sketch model is not a translator — it is a re-representer. It takes the mathematical ideas expressed in the natural-language proof and re-expresses them in a form (lemma decomposition) that is native to the formal proving paradigm. The rubric RL training ensures this re-representation is faithful (lemmas are mathematically valid and aligned with the proof strategy) while also being useful (lemmas are self-contained, appropriately sized, and genuinely decompositional). This is a form of semantic compilation: the natural-language proof provides the specification, and the sketch model produces an implementation plan in the formal language.

Why this matters for the formal-natural language debate. The paper's opening question — "Is pursuing formal theorem proving with LLMs still a viable and valuable path?" — reflects genuine tension in the field. If LLMs can produce rigorous natural-language proofs at a fraction of the cost of formal proofs, and if natural-language proofs are "good enough" for most applications, then formal proving looks like an expensive luxury. The paper's answer — "yes, but only if we leverage natural-language capabilities to accelerate formal proving" — reframes the relationship from competition to symbiosis. The sketch model is the mechanism that enables this symbiosis: it allows the formal system to benefit from the natural-language prover's broad reasoning capability (trained on vast informal mathematical text) while the agentic prover provides the verification guarantee that natural-language proving lacks.

This symbiosis is evidenced by the test-time scaling behavior (Figure 6a): the log-linear improvement in solve rate with increased compute budget suggests that the decomposition strategy is effectively converting compute into problem-solving capability. If the sketch model were producing poor decompositions, additional compute spent on the agentic prover would yield diminishing returns (the prover would be attempting to prove ill-conceived lemmas). The fact that more compute continues to yield more solved problems implies that the decompositions are generally sound — the agentic prover's failures are due to the inherent difficulty of the lemmas, not to the sketch model providing impossible or irrelevant targets.

The recursive decomposition loop as a form of learned problem reduction. The test-time workflow's ability to recursively decompose failed lemmas (applying the natural-language→sketch→agent pipeline to sub-goals) means the system can dynamically adjust its decomposition granularity based on the agentic prover's actual capabilities. If a lemma is too hard to prove directly, it gets further decomposed. If a lemma is disproved, the decomposition gets revised. This is a form of adaptive problem reduction — the system searches over the space of possible decompositions, using the agentic prover's success/failure as a signal about whether the current decomposition is at an appropriate level of granularity. This is fundamentally different from fixed decomposition strategies (e.g., always breaking a proof into 5 lemmas) or monolithic approaches (no decomposition at all). It is a learned, dynamic strategy that emerges from the interaction between the sketch model's generative capability and the agentic prover's verification capability.

Innovation 5: The Demonstration That Formal Proving's Efficiency Gap With Natural Language Is Narrowing, Not Intrinsic

The paper's headline result — solving 11 out of 12 Putnam 2025 problems within 9 hours — is not just a performance milestone. It is evidence for a specific and important empirical claim: the efficiency gap between formal and natural-language theorem proving is not a fundamental limitation of formal methods, but an artifact of suboptimal interaction and training paradigms. Prior work (most starkly AlphaProof at 500 TPU-days per problem for 56% on PutnamBench) suggested that formal proving imposed an irreducible overhead — the cost of mechanical verification, the verbosity of formal syntax, the lack of informal reasoning shortcuts. Seed-Prover 1.5's performance at 10 H20-days per problem for 88% on PutnamBench suggests that much of this overhead was not due to formal verification per se, but to inefficient use of the formal environment.

What changed. The paper does not introduce a fundamentally faster proof checker, a more compact formal language, or a breakthrough in search algorithms. The efficiency gains come entirely from organizational improvements: the agentic prover's learned interaction strategy (avoiding redundant tool calls, internalizing knowledge, caching verified lemmas), the sketch model's decomposition (breaking intractable monolithic proofs into tractable sub-problems), and the test-time workflow's parallelization (attacking independent lemmas simultaneously). These are all "software engineering" improvements in the broadest sense — better ways of using existing tools — rather than fundamental algorithmic advances. The implication is that the formal proving community has been leaving enormous efficiency on the table by clinging to fixed interaction paradigms (step-level or whole-proof) rather than allowing models to learn adaptive strategies.

The significance for the field's trajectory. If formal proving's efficiency gap were intrinsic — if mechanical verification inherently costs 100× more than informal reasoning — then the practical case for formal methods would rest entirely on applications where correctness guarantees are non-negotiable (safety-critical systems, mathematical research infrastructure). But if the gap can be narrowed to within a factor of 2-5× through better interaction design and RL training, the domain of practical applicability expands dramatically. Seed-Prover 1.5's performance puts formal proving within striking distance of natural-language systems for undergraduate and graduate-level mathematics: 88% on PutnamBench is not yet the near-perfect scores of DeepSeek-Math-V2 on Putnam 2024, but it is close enough to suggest that the remaining gap might be bridgeable through further scaling of the RL training and test-time compute, rather than requiring fundamental breakthroughs.

The counter-evidence from hard problems. The paper is careful not to overclaim: on Fate-X (PhD-level problems), performance remains at 33%, and on the Erdős problems, the system solved only "mathematically relatively simple" instances or trivial/simplified versions. This establishes a boundary condition: the efficiency gains from better interaction paradigms apply primarily within the model's capability range. On problems that genuinely require knowledge beyond the training distribution (advanced graduate-level mathematics, frontier research conjectures), the model still struggles. This is consistent with the broader finding from LLM scaling research — improved training and inference methods amplify existing capabilities but do not create fundamentally new ones. The implication is that formal proving's efficiency gap with natural language has two components: an interaction overhead (which can be reduced through better system design and RL training) and a capability gap (which can only be closed through better pretraining, more data, or fundamentally more capable models). Seed-Prover 1.5 demonstrates that the interaction overhead was much larger than previously appreciated, but it does not eliminate the capability gap — and the paper's honest reporting of Fate-X and Erdős results makes this boundary clear.

The compute budget comparison as a diagnostic tool. Table 2's comparison of compute budgets tells a specific story: AlphaProof used 500 TPU-days/problem for 56.1% on PutnamBench; Hilbert used an average of 1840 attempts per problem for 70.0%; Aleph Prover used an average of 1834 tool calls for 75.8%; Seed-Prover 1.0 used 18 H20-days/problem for 50.4%; Seed-Prover 1.5 uses 10 H20-days/problem for 87.9%. The progression is not monotonic — Hilbert and Aleph achieve higher performance than Seed-Prover 1.0 but use different compute metrics, making direct comparison difficult. But the overall trajectory is clear: the field is simultaneously improving capability and reducing cost, with Seed-Prover 1.5 representing a Pareto improvement over prior systems in the capability-per-compute tradeoff. This pattern — simultaneous improvement in both axes — is characteristic of a field moving from artisanal (each system hand-crafted for a specific benchmark) to engineered (general principles are being discovered that transfer across systems). The paper's contribution to this trend is identifying learned interaction strategy and learned decomposition as two such general principles, not just system-specific optimizations.

5. Experimental Analysis

Evaluation Methodology

Dataset. The paper evaluates on five benchmarks: PutnamBench [21] (660 problems from the Putnam Mathematical Competition, spanning 1962–2024, described as "undergraduate-level"), FATE [10] (split into Fate-H with 100 problems at "honors course exams or graduate-level difficulty" and Fate-X with 100 problems at "PhD qualifying exams or beyond"), CombiBench [14] (a combinatorial mathematics benchmark, though the paper notes "significant formalization issues within this dataset" and lists results "for reference"), IMO 2025 (6 problems), and Putnam 2025 (12 problems). A subset of 200 PutnamBench problems, named Putnam-200, is used for fast evaluation during RL training checkpoint selection. For frontier mathematics assessment, the paper also tests on a curated subset of problems from the Erdős problem set, filtered to remove formalization errors (e.g., Erdős-74, 590, 591).
Base model(s). The agentic prover is post-trained from the Seed-Prover 1.0 model [3], which itself is based on an unspecified base LLM architecture (the paper provides minimal detail about the underlying pretrained model). The Natural Language Prover is initialized from Doubao-Seed-1.6, a separate LLM optimized for natural language reasoning. The magnitude of these models (parameter count, pretraining data) is not disclosed. The paper argues that Seed-Prover 1.0 is "representative of the capabilities" [3] needed for formal theorem proving and that post-training it into an agentic prover demonstrates the scaling potential of the agentic RL approach, but the absence of architectural detail makes it difficult to assess how much of the performance derives from the base model's capabilities versus the training methodology.
Metrics. The primary metric is solve rate: the fraction of problems for which the system produces a formally verified Lean proof of the target theorem. This is a binary per-problem measure — a problem is either solved (a complete, compiler-accepted proof is produced within the compute budget) or not. The paper also reports training-level metrics during RL: batch-level training accuracy (the fraction of training batch problems successfully proved by the current policy), average number of function calls per trajectory (a measure of tool-use efficiency), average total sequence length in tokens (a measure of context efficiency), and average score on samples grouped by response length (a proxy for long-horizon reasoning capability). For the test-time scaling analysis, the metric is total number of PutnamBench problems solved as a function of compute budget.
Baselines. The paper compares against several state-of-the-art formal provers: AlphaProof [8] (56.1% on PutnamBench, using 500 TPU-days per problem), Hilbert Prover [22] (70.0% on PutnamBench, using an average of 1840 attempts per problem), Aleph Prover (75.8% on PutnamBench, using an average of 1834 tool calls), Seed-Prover 1.0 [3] (50.4% on PutnamBench and 35% on Fate-H, using 18 H20-days per problem in its "medium" workflow), Goedel-Prover-V2-32B [13] (86/660 on PutnamBench, 2/100 on Fate-H, 0/100 on Fate-X, under pass@64), and Aristotle [1] (IMO-level theorem proving). For the agentic prover alone (without the test-time workflow), the primary comparison is against Seed-Prover 1.0's medium workflow under a compute-equivalent setting (Pass@8×8 for the agentic prover versus the 1.0 medium workflow's more expensive resource allocation).
Generation budget / compute accounting. The paper measures compute in H20-days per problem, where one H20-day represents 24 hours of computation on a single H20 GPU. This metric accounts for both the model's generation cost and the tool execution overhead (Lean compilation, mathlib search, Python execution). For the agentic prover, a Pass@k×m budget means k independent trajectories, each allowed up to m summarization-based retries under the light inference protocol — so the maximum total attempts per problem is k×m, though in practice many trajectories succeed early and consume less than the full budget. The test-time workflow's compute budget aggregates compute across the Natural Language Prover, Sketch Model, and Agentic Prover, including the recursive decomposition overhead. For baseline comparison, the paper notes that H20-days and TPU-days are not directly comparable metrics, and that different systems report compute in different units (attempts, tool calls, GPU/TPU-days), making precise cost-normalized comparison difficult. The paper's key compute claim is qualitative: Seed-Prover 1.5 achieves higher performance than prior systems while using less compute within the H20-day metric.
Cross-validation / statistical protocol. For RL training checkpoint selection, the paper uses the Putnam-200 subset (200 problems from PutnamBench) to evaluate checkpoint performance at different training steps, selecting the best-performing checkpoint (at the 1055th training step) for final evaluation. This approach avoids contaminating the full PutnamBench test set with checkpoint selection decisions, but does not constitute formal cross-validation — there is no fold-based rotation or statistical testing. For the test-time scaling analysis, the paper reports total solve counts as a function of compute budget (Figure 6a) and a histogram of solve times (Figure 6b), but does not provide confidence intervals, error bars, or statistical significance tests for any performance numbers. The Erdős evaluation is described as qualitative: the paper lists solved problem numbers but acknowledges that some are "mathematically relatively simple" or represent "trivial or simplified versions" due to misformalization.

Main Quantitative Results

Agentic Prover Training Dynamics

The RL training of the agentic prover produces substantial improvements across multiple dimensions simultaneously. Figure 3a shows that batch-level training accuracy — the fraction of training batch problems successfully proved by the current policy — increases from approximately 50% at initialization to nearly 90% after 1000+ RL steps. This is a roughly 40 percentage point improvement from the SFT cold-start model to the fully RL-trained model, indicating that the RL signal from Lean verification is providing rich learning despite being sparse and binary.

The improvement transfers to held-out benchmarks. Figure 3b tracks performance on the Putnam-200 subset for two evaluation settings: direct proving (Pass@8×1 — eight independent trajectories with no summarization-based retries) and light inference (Pass@8×8 — eight trajectories with up to eight retries each). Both curves increase monotonically with RL training steps, with the light inference setting consistently outperforming direct proving by a widening margin. At the final checkpoint (step 1055), the light inference accuracy on Putnam-200 is approximately double the direct proving accuracy, demonstrating that the RL training not only improves the model's first-attempt capability but also its ability to effectively use summarization-based retries — an emergent skill that was not explicitly rewarded during training (the reward is purely outcome-based, not process-based).

The paper selects the 1055th-step checkpoint for full benchmark evaluation. Table 1 compares this agentic prover against Seed-Prover 1.0's medium workflow on the full PutnamBench and FATE benchmarks:

Approach	Budget	Putnam	Fate-H	Fate-X
Seed-Prover 1.0 (medium)	18 H20 days/problem	331/660	35/100	9/100
Seed-Prover 1.5 (agentic only)	Pass@8×8	359/660	57/100	10/100

The agentic prover solves 28 more PutnamBench problems (359 vs. 331, representing a ~8.5% relative improvement) and 22 more Fate-H problems (57 vs. 35, representing a ~63% relative improvement) while using a lighter compute budget (Pass@8×8 versus the 1.0 medium workflow's 18 H20-days per problem). On Fate-X, the improvement is marginal (10 vs. 9 problems), consistent with the paper's narrative that PhD-level problems remain fundamentally challenging and beyond the current model's effective capability range.

The behavioral changes underlying these performance improvements are documented in Figure 4, which tracks four training metrics across 1200 RL steps:

Average number of function calls per trajectory (Figure 4a): Drops from approximately 15 calls at initialization to 10 calls at step 1200. The model learns to be more strategic about when to invoke tools — it no longer engages in the "trial-and-error" invocations characteristic of the SFT model, instead calling tools only when they serve a clear purpose in advancing the proof.
Average total sequence length (Figure 4b): Decreases from approximately 28,000 tokens to 17,000 tokens, a ~39% reduction. This is partially a consequence of fewer function calls (each call and its response consume context tokens), but also reflects the model learning to produce more concise natural-language reasoning and more targeted Lean code.
Score of long-horizon responses (Figure 4c, 4d): For samples with response lengths in the 16K–32K range, the average score (a proxy for proof success) improves from near zero at initialization to ~0.6 by step 1200. For the 32K–64K range, improvement is visible but more modest and more variable — scores remain in the −0.2 to 0.4 range with high variance, indicating that "effectively reasoning over extremely long contexts remains a challenge" (Section 4.1).

Figure 5 provides the most nuanced evidence of learned behavioral change: the distribution of mathlib search calls per trajectory for successfully proved problems, comparing an intermediate checkpoint (step 495) with the final checkpoint (step 1055). On PutnamBench, the proportion of proved samples using ≤10 search calls increases from 71.1% to 79.7% between the two checkpoints, while the proportion using >20 search calls drops from 9.1% to 8.9% — a modest shift toward fewer searches. On Fate-H, the shift is more dramatic: the proportion using ≤10 search calls increases from 31.7% to 45.6% , while the proportion using >20 search calls drops from 53.7% to 45.6% . The paper interprets this as "internalizing knowledge from search results" — the model learns which theorems are available in mathlib and retrieves them from its parameters rather than through explicit search calls, an efficiency gain that compounds with the tool-call reduction seen in Figure 4a.

Full System Performance on PutnamBench, FATE, and CombiBench

Table 2 presents the central benchmark results for the complete Seed-Prover 1.5 system (agentic prover + sketch model + test-time workflow) compared against state-of-the-art formal provers:

System	Compute Budget	Putnam	Fate-H	Fate-X	CombiBench
Seed-Prover 1.0 (medium)	18 H20 days/problem	50.4%	35%	9%	39%
AlphaProof	500 TPU days/problem	56.1%	—	—	—
Hilbert	avg pass@1840	70.0%	—	—	—
Aleph Prover	avg 1834 tool calls	75.8%	—	—	—
Seed-Prover 1.5	10 H20 days/problem	580/660 (87.9%)	80%	33%	48%

On PutnamBench, Seed-Prover 1.5 solves 580 out of 660 problems (87.9%) . This represents an absolute improvement of 37.5 percentage points over Seed-Prover 1.0 (50.4% → 87.9%), 31.8 points over AlphaProof (56.1% → 87.9%), 17.9 points over Hilbert (70.0% → 87.9%), and 12.1 points over Aleph Prover (75.8% → 87.9%). The compute budget of 10 H20-days per problem is approximately 44% less than Seed-Prover 1.0's 18 H20-days per problem, though direct comparison with AlphaProof's 500 TPU-days is complicated by the different hardware metrics.

On Fate-H, Seed-Prover 1.5 solves 80 out of 100 problems (80%) , a 45 percentage point improvement over Seed-Prover 1.0's 35% and more than doubling the solve rate. No prior system reported Fate-H results, making this the first benchmark establishment for graduate-level formal theorem proving at this scale.

On Fate-X, Seed-Prover 1.5 solves 33 out of 100 problems (33%) , a substantial improvement over Seed-Prover 1.0's 9% (a ~3.7× relative improvement) but still far from saturation. This is consistent with the paper's honest assessment that PhD-level problems "remain challenging and beyond the model's effective capability range" due to the "increased complexity and limitations in Mathlib support."

On CombiBench, Seed-Prover 1.5 achieves 48% versus Seed-Prover 1.0's 39%. However, the paper explicitly caveats these results, noting "significant formalization issues within this dataset" and stating the numbers are "for reference." The 9 percentage point improvement is suggestive but should be treated cautiously given the acknowledged benchmark quality issues.

Compute budget interpretation caveat. The 10 H20-days per problem budget reported in Table 2 includes all three agents (Natural Language Prover, Sketch Model, Agentic Prover) and the recursive decomposition overhead. However, the paper does not break down how this budget is distributed across agents or problem difficulty levels. For problems that are solved quickly (the majority, based on Figure 6b showing most solves within the first few hours), the actual compute consumed is far less than 10 H20-days — the budget is a cap, not an average. The comparison with Seed-Prover 1.0's 18 H20-days (which also includes its medium workflow overhead) and AlphaProof's 500 TPU-days (which includes extensive search) is qualitatively informative but not precisely quantitative due to the different compute measurement conventions.

Test-Time Scaling Behavior

Figure 6 analyzes how the complete Seed-Prover 1.5 workflow scales with computational budget on PutnamBench. Figure 6a plots total solved problems against compute budget (measured in H20-days per problem), revealing a log-linear relationship: each doubling of the compute budget produces a roughly constant increment in solved problems. The curve shows seed prover 1.5 moving from approximately 300 solved problems at 1 H20-day per problem to approximately 580 solved problems at 10 H20-days per problem. The log-linear scaling is significant because it implies sustained returns to additional compute — the system is not saturating, and further budget increases would be expected to yield further improvements (albeit with diminishing marginal returns, as the log-linear slope is shallow).

Figure 6b shows the distribution of solve times per problem. The histogram reveals a heavy-tailed distribution: the majority of problems are solved within the first few hours (the leftmost bar is the tallest), but a long tail of harder problems is distributed across the 9–53 hour range, with some problems requiring the full 53-hour search duration. This pattern is characteristic of systems where easy problems are rapidly dispatched by the initial decomposition and proving attempts, while hard problems require deep recursive decomposition (up to the maximum search depth of 8, achieved through the restart mechanism that effectively doubles the initial depth-4 limit) and extensive exploration of alternative lemma structures.

The paper does not provide a breakdown of which PutnamBench problems fall into which solve-time bucket, nor does it correlate solve time with problem difficulty (e.g., whether the long-tail problems correspond to the hardest difficulty bins from prior PutnamBench difficulty categorizations). This limits the diagnostic value of the histogram — we can observe that the distribution is heavy-tailed, but we cannot determine whether the tail represents inherently harder mathematics or merely problems where the sketch model's initial decomposition was suboptimal.

IMO 2025 and Putnam 2025 Results

Table 3 reports the solve times for IMO 2025 problems. Seed-Prover 1.5 solved 5 out of 6 problems (problems P1, P2, P3, P4, and P5; P6 is marked with "X" indicating failure), with solve times ranging from 0.01 hours for P2 (solved by a separate geometry-focused component, Seed-Geometry) to 16.5 hours for P1. The paper notes that while Seed-Prover 1.0 required its "Heavy" mode to solve 5 out of 6 IMO problems, Seed-Prover 1.5 achieved the same solve rate "using compute resources comparable to the 1.0 'Medium' setting (20 H20-days/problem), with a significantly shorter runtime than Seed-Prover 1.0 (Heavy)."

This claim is noteworthy but underspecified: the paper does not provide the exact compute budget used for IMO 2025, the specific runtime of Seed-Prover 1.0 Heavy for comparison, or a problem-by-problem breakdown of compute consumed. The 0.01-hour solve time for P2 is striking — sub-minute solving implies the problem was either trivially within the model's capability or that the geometry-specific component had a highly targeted solution path. The 16.5-hour solve time for P1 suggests a much harder struggle, consistent with a problem that required deep recursive decomposition and multiple retries.

Table 4 reports the solve times for Putnam 2025 — the paper's marquee result. Seed-Prover 1.5 solved 11 out of 12 problems within a 9-hour window, using a maximum compute budget of 40 H20-days per problem (the budget was not fully consumed since all 11 solved problems completed within 9 hours). Solve times range from 0.5 hours (A2, B3) to 9 hours (B1). Problem A5 is marked with "X" (unsolved). The paper notes that the prover "is not using any 'native_decide' in Putnam, which is unsafe under Lean" — a methodological detail indicating that the proofs are constructed using standard Lean tactics rather than relying on decision procedures that might be considered too powerful or that might not scale to general theorem proving.

The 11/12 result on Putnam 2025 is the paper's strongest single performance claim. The 9-hour wall-clock completion time demonstrates that the parallel decomposition strategy (attacking independent lemmas simultaneously) converts the compute budget into practical speed — the system did not need to run for the full 40 H20-day budget because parallel work on independent lemmas enabled rapid completion. However, the paper does not provide a detailed trace for the unsolved problem (A5), making it impossible to diagnose whether the failure was due to insufficient decomposition, lack of required mathlib theorems, fundamental capability limitations, or some other cause.

Erdős Problem Set

The paper reports that Seed-Prover 1.5 solved problems numbered 124, 198, 303, 316, 330, 350, 370, 379, 418, 449, 493, 499, 645, 728, and 958 from the Erdős problem set. However, the authors immediately qualify this result with unusual candor:

"based on our observations, these problems are mathematically relatively simple, or we proved a trivial or simplified version of them due to mis-formalization (these mis-formalized problems are not listed here)"

This is effectively a negative result: the system's Erdős performance does not demonstrate capability on frontier mathematical conjectures. The problems solved are either simple enough to be within the model's existing capability or were solved due to formalization errors that made them easier than intended. The paper states that "our systems, whether using natural language or formal language, are still some distance away from truly helping to advance research on frontier open mathematical problems."

This honest assessment is methodologically valuable, even if the result itself is modest. It establishes a clear capability boundary: Seed-Prover 1.5 masters competition-style problems at the undergraduate and graduate level but does not yet generalize to the open-ended, research-frontier mathematics represented by the Erdős conjectures. The paper attributes this limitation to a "critical dependency issue" — frontier mathematics requires synthesizing insights across a multitude of research papers, identifying relevant prior work, and formalizing not just the target theorem but the entire dependency chain of results it relies on. The current system, trained primarily on competition problems and formalized textbooks, lacks the breadth of mathematical knowledge needed for this task.

Agentic Prover vs. Seed-Prover 1.0: Ablation of the Agentic Paradigm

Table 1 serves as an implicit ablation study: by comparing the agentic prover alone (without the sketch model or test-time workflow) against Seed-Prover 1.0, we can isolate the contribution of the agentic interaction paradigm and RL training from the contributions of decomposition and test-time scaling.

The agentic prover under Pass@8×8 solves 359/660 on PutnamBench versus Seed-Prover 1.0 medium's 331/660. This +28 problem improvement comes from the agentic paradigm alone — better tool use, incremental lemma caching, and RL-learned interaction strategies — without any decomposition assistance. On Fate-H, the improvement is more dramatic: 57/100 versus 35/100 (+22 problems, a 63% relative improvement). This suggests that graduate-level problems, which rely more heavily on mathlib knowledge and careful lemma management, benefit disproportionately from the agentic prover's ability to search for and internalize relevant theorems.

However, the agentic prover alone (359/660) falls far short of the full system (580/660). The additional 221 problems solved by the complete system represent the contribution of the sketch model and test-time workflow — decomposition of complex theorems into tractable sub-goals, which enables the agentic prover to tackle problems it cannot solve monolithically. This confirms that the agentic paradigm and the decomposition paradigm are complementary rather than redundant: the agentic prover provides efficient lemma-level execution, and the sketch model provides the structural decomposition that makes complex theorems accessible to that execution.

Ablation Studies and Robustness Checks

RL training data filtering: The paper describes a filtering procedure (Section 3.2) where problems that the SFT model proves more than three times are excluded from RL training, and problems that cannot be proved under any prompting strategy are also removed. This filtering is not formally ablated (the paper does not train an RL model on unfiltered data for comparison), but the training dynamics curves (Figures 3a, 3b) serve as implicit validation: the monotonic improvement in both training and test accuracy suggests the filtering succeeded in focusing RL on problems where improvement was possible without creating a training distribution too narrow to generalize. The retention of "context-dependent" problems (provable with summarization but not directly) is an interesting design choice that is not separately evaluated — we cannot determine whether these problems contributed disproportionately to the model's improvement on the direct proving setting.

RL reward function design: The binary +1/−1 reward function (success = +1, anything else = −1) is not ablated against alternatives. The paper does not compare against a +1/0 reward (rewarding success but not penalizing failure), a shaped reward (providing partial credit for progress, such as number of lemmas proved or fraction of the proof completed), or a reward incorporating efficiency penalties (explicitly penalizing excessive tool calls or sequence length). This is a significant missing ablation because the binary penalty on failure (−1 rather than 0) creates an incentive for the model to avoid budget-exhausting trajectories, which might partially explain the efficiency improvements observed in Figure 4. Without the ablation, we cannot distinguish whether the efficiency gains are intrinsic to agentic RL or specific to the −1 failure penalty.

Search call distribution analysis (Figure 5): The observation that search calls decrease while performance improves is treated as evidence of "internalization." However, the paper does not control for a simpler explanation: later checkpoints might simply be solving different problems (easier ones where search is unnecessary) while still failing on the hard problems that require extensive search. The fact that the total solve count increases while the distribution shifts toward fewer searches is evidence against this alternative — but the paper does not provide a problem-level analysis showing that the same problems that required many searches in early checkpoints require fewer searches in later checkpoints. Such an analysis would conclusively demonstrate internalization.

Sketch model rubric design: The rubric-based reward for the sketch model (Equation 2: reward +1 only if N_lemmas ≥ 3 AND S_FL ≥ 0 AND S_NL ≥ 0.7) is evaluated indirectly through the full system's performance but is not directly ablated. The paper does not compare against: (1) a simpler reward function using only Lean structural verification (no NL quality component), (2) a reward function using a scalar LLM judge rather than the structured rubric, (3) a reward function with different lemma count thresholds (e.g., N_lemmas ≥ 1 or N_lemmas ≥ 5), or (4) SFT-only training of the sketch model without RL. This makes it difficult to attribute the sketch model's effectiveness specifically to the rubric-based RL rather than to the underlying model quality or the natural-language prover's proof quality.

Recursive decomposition depth and restart mechanism: The test-time workflow's maximum search depth (4, extended to 8 via restart) is not ablated. The paper does not report performance at different depth limits (e.g., depth 2, 3, 4 without restart, 4 with restart) to quantify how much the recursive decomposition and restart mechanism contribute over simpler decomposition strategies. The restart mechanism itself — incorporating proven lemmas from a failed first attempt and retrying from scratch — is an interesting design choice that is not evaluated independently. A comparison against simply allowing deeper initial search (depth 8 without restart) would reveal whether the restart's partial progress preservation is beneficial or whether it just simulates deeper search at similar cost.

Pass@k×m budget sensitivity: The paper uses Pass@3×3 for the agentic prover within the test-time workflow and Pass@8×8 for standalone agentic prover evaluation. The sensitivity of performance to these budget choices is not explored. Would Pass@2×4 outperform Pass@4×2? Would Pass@1×9 (more retries, fewer independent trajectories) be more efficient for hard lemmas where the first attempt is usually wrong but partial progress enables recovery? This budget allocation tradeoff — parallel exploration versus sequential refinement — is analogous to the sequential-versus-parallel sampling analysis in prior test-time compute work but is not studied here.

Natural Language Prover quality: The Natural Language Prover (initialized from Doubao-Seed-1.6) is a critical component of the test-time workflow because it generates the natural-language proofs that the sketch model decomposes. The paper does not ablate the quality of this component — e.g., by comparing against a weaker natural language prover or by using ground-truth human-written proofs instead of LLM-generated ones. This makes it unclear whether the system's performance depends on having a state-of-the-art natural language prover or whether the sketch model and agentic prover can recover from lower-quality natural language proofs.

Tool call limit and sequence length limit: The agentic prover's interaction budget — maximum 64K tokens and maximum 28 tool calls — is stated (Section 3.1) but its impact on performance is not abated. The paper does not report how often trajectories hit these limits, whether failed trajectories typically exhaust the token budget or the tool call budget first, or whether relaxing these limits would improve performance (particularly for the long-horizon problems that Figure 4d shows remain challenging). The 64K token limit is substantial by current standards but might constrain proofs that require extensive lemma development, particularly on Fate-X problems where the model's 33% solve rate suggests the limit is not the primary bottleneck.

Checkpoint selection protocol: The best-performing RL checkpoint (step 1055) is selected based on Putnam-200 performance, creating a potential indirect form of test-set leakage: the full PutnamBench evaluation (660 problems) contains 200 problems from Putnam-200. The paper does not state whether the checkpoint selection was done with Putnam-200 excluded from the training data, or whether the Putnam-200 results in Figure 3b represent held-out evaluation or training-set evaluation. If Putnam-200 was part of the RL training data, the selection criterion would be biased toward checkpoints that overfit the training distribution, and the reported 87.9% on full PutnamBench might not reflect the performance of a checkpoint selected via a truly held-out validation procedure.

Single-model evaluation vs. best-of-ensemble: All evaluations use a single checkpoint (step 1055) of the RL-trained model. The paper does not explore whether ensembling multiple checkpoints (e.g., majority voting across checkpoints from steps 900, 1000, 1100, 1200) would yield additional performance improvements, or whether the single-checkpoint performance is representative of the training run's stability (i.e., do nearby checkpoints have similar performance, or is there high variance that makes the step-1055 result unusually favorable?).

Compute accounting consistency: The paper reports compute budgets in H20-days per problem but does not detail how this metric is computed for the complete test-time workflow. Specifically: (1) How are tool execution costs (Lean compilation, mathlib search, Python execution) amortized into the H20-day metric? (2) Does the recursive decomposition overhead (running the Natural Language Prover and Sketch Model multiple times for deeply nested decompositions) get charged to the problem's budget? (3) For problems solved quickly (e.g., A2 at 0.5 hours in Putnam 2025), is the "10 H20-days per problem" budget still reported, or is actual consumption reported? The paper's compute claims (e.g., "more efficient than prior systems") depend on the consistency of this accounting, and the lack of detail makes independent verification difficult.

Critical Assessment

Claim 1: "Agentic RL training produces substantial improvement in formal theorem proving capability, with the RL-trained model significantly outperforming the SFT baseline."

The evidence for this claim is strong for the specific models and benchmarks tested. Figure 3a shows training accuracy improving from ~50% to ~90% over 1200 RL steps. Table 1 shows the RL-trained agentic prover solving 359/660 on PutnamBench versus the SFT-based Seed-Prover 1.0's 331/660 (under the same benchmark, though not exactly the same compute budget — the 1.0 used a more expensive "medium" workflow). On Fate-H, the improvement is 57/100 versus 35/100.

However, the claim is narrower than "RL improves formal theorem proving capability" — it demonstrates that VAPO-based RL with outcome rewards, applied to an SFT-warm-started agentic prover, on a filtered dataset of challenging-but-provable problems, improves performance on competition-style benchmarks. Whether alternative RL algorithms, reward structures, or training data compositions would produce similar or greater improvements is unexplored. The absence of ablation on the binary negative reward (−1 for failure) means we cannot determine whether the efficiency improvements (Figure 4) are intrinsic to agentic RL or specific to the penalty structure that incentivizes avoiding budget-exhausting trajectories.

Additionally, the SFT baseline is not a static target — the paper's filtering procedure (Section 3.2) removes problems that the SFT model proves reliably, focusing RL on a harder subset. If the SFT model were evaluated on the full unfiltered dataset, its performance might be higher than the 331/660 reported in Table 1 (which is on PutnamBench, not the training set). The comparison in Table 1 is between the RL model evaluated on the full PutnamBench and the SFT-based Seed-Prover 1.0 also evaluated on the full PutnamBench — but the RL model was trained on a filtered subset that excluded problems the SFT model could already solve. This means the RL model's training distribution was harder than the SFT model's, making the performance improvement potentially more impressive (the model got better while training on harder data) but complicating the SFT-vs-RL comparison (the SFT model may have been overtrained on easy problems that were filtered out for RL).

The most convincing evidence for RL's contribution is the combination of Figures 3a (monotonic training improvement), 3b (monotonic test improvement), 4 (efficiency improvements), and 5 (adaptive search behavior changes). No single metric is dispositive, but the convergence of multiple indicators — all pointing toward the same conclusion that RL is producing genuine capability gains — makes the claim credible.

Claim 2: "The agentic paradigm (lemma-level interaction with incremental caching) is more efficient than both step-level and whole-proof paradigms."

This claim is supported indirectly through the comparison with prior systems in Table 2 and the efficiency metrics in Figure 4, but not through direct head-to-head comparison. The paper does not train a step-level prover and a whole-proof prover using the same base model, same training data, and same RL algorithm, then compare their efficiency. Instead, it compares against published results from different systems (AlphaProof, Hilbert, Aleph, Seed-Prover 1.0) that used different models, different training procedures, and different compute metrics.

Specifically:

The comparison with AlphaProof (56.1% at 500 TPU-days/problem) uses different hardware and different base models. AlphaProof was a much earlier system; it is possible that improvements since AlphaProof's publication (in base model quality, training techniques, etc.) account for some of the performance gap.
The comparison with Hilbert (70.0% at avg 1840 attempts) uses different compute metrics (attempts vs. H20-days). Converting between these metrics requires assumptions about model size, hardware efficiency, and per-attempt cost that the paper does not provide.
The comparison with Aleph Prover (75.8% at avg 1834 tool calls) is the most informative because both systems use tool-call counts as a metric, but Aleph's tool calls are not the same type as Seed-Prover 1.5's — Aleph's tool calls might represent a mixture of Lean verification and search queries at different granularities.

The strongest evidence for the agentic paradigm's efficiency comes from the within-system comparison: Seed-Prover 1.0 (whole-proof paradigm) versus Seed-Prover 1.5 agentic prover alone (Table 1). This compares two models that share the same lineage (1.5 is post-trained from 1.0), evaluated on the same benchmarks, with performance reported in comparable units. The agentic prover achieves higher performance (359 vs. 331 on Putnam, 57 vs. 35 on Fate-H) while using a lighter compute budget (Pass@8×8 vs. 18 H20-days/problem). This is the paper's best evidence that the agentic paradigm is more efficient — but it remains a single comparison between two specific implementations, not a systematic ablative study.

The claim about lemma-level caching specifically (as opposed to other aspects of the agentic paradigm, such as dynamic tool use or RL training) is not isolated. The paper never compares a version of the agentic prover without caching against the version with caching. The efficiency benefits attributed to caching (Section 3.1: alignment with modular proofs, decomposition of complexity, context efficiency, flexible inference control) are theoretical arguments buttressed by the overall system's efficiency, not empirically verified mechanisms.

Claim 3: "The sketch model, trained via rubric-based RL, effectively bridges natural-language proofs and formal Lean decompositions, enabling the agentic prover to solve problems it cannot solve monolithically."

The evidence for this claim comes from the performance gap between the agentic prover alone (359/660 on Putnam, Table 1) and the full system (580/660 on Putnam, Table 2). The additional 221 solved problems must be attributed to some aspect of the full system that the agentic prover alone lacks — most plausibly, the sketch-driven decomposition that breaks complex theorems into tractable sub-goals.

However, the full system also includes:

The Natural Language Prover (initialized from Doubao-Seed-1.6), which the agentic prover alone does not have access to. Some of the improvement might come from the natural-language prover's reasoning capability, not from the sketch model's decomposition.
The test-time orchestration (recursive decomposition, parallel lemma proving, sketch refinement on disproof), which the agentic prover alone lacks. Some of the improvement might come from the test-time workflow's search over decomposition strategies, not from the sketch model's specific training.

The paper does not provide ablation experiments that isolate the sketch model's contribution from these other components. For example: (1) what is the performance of the full system using an untrained sketch model (e.g., the base model prompted to produce lemma sketches without rubric RL)? (2) What is the performance using the Natural Language Prover's output directly as input to the agentic prover, without the sketch model's decomposition step? (3) What is the performance of the agentic prover with the test-time workflow's recursive decomposition but without the sketch model (e.g., using a simpler decomposition heuristic)?

The rubric-based RL training methodology itself is not directly validated. The paper does not compare the rubric-trained sketch model against a sketch model trained with a simpler reward (e.g., only Lean structural verification) or against an SFT-only sketch model. The detailed rubric prompts in Appendix B are impressive engineering, but whether they produce better sketch models than simpler approaches is an empirical question the paper does not answer.

Claim 4: "Test-time compute scaling produces log-linear improvements in solve rate, with sustained returns to additional compute."

Figure 6a provides clear evidence for log-linear scaling on PutnamBench over the range of 1–10 H20-days per problem. Each doubling of the compute budget produces a roughly constant increment in solved problems, with no visible saturation at 10 H20-days. This supports the claim that additional compute would yield further improvements.

However, the claim is limited to PutnamBench over this specific compute range. The paper does not demonstrate log-linear scaling on Fate-H or Fate-X (no equivalent Figure 6 for those benchmarks). The scaling curve might plateau at higher compute budgets not tested (e.g., 20, 40, 80 H20-days per problem). The heavy-tailed solve time distribution (Figure 6b) suggests that the marginal problems solved with additional compute are increasingly hard, which means the log-linear relationship might break down when the system hits problems that fundamentally exceed its capability — at which point additional compute would produce zero return, not diminishing return.

The scaling analysis also does not decompose where the additional compute is being spent. Is it enabling deeper recursive decomposition? More parallel lemma-proving attempts? More retries on individual lemmas? Without this decomposition, it is unclear whether the log-linear scaling is a fundamental property of the test-time workflow or an artifact of the specific budget allocation strategy (e.g., spending more compute on Pass@k×m for harder problems).

Claim 5: "The efficiency gap between formal and natural-language theorem proving is narrowing, not intrinsic."

The Putnam 2025 result — 11/12 problems solved within 9 hours — is the paper's strongest evidence for this claim. A system that can solve nearly all of the most recent Putnam competition problems in less than a workday's worth of computation represents a dramatic improvement over AlphaProof's 500 TPU-days per problem to solve 56% of a broader Putnam set. If these results are replicable (the paper's model and weights are released, enabling independent verification), they genuinely shift the conversation about formal proving's practical viability.

However, the claim operates at a qualitative level that the quantitative results only partially support:

Putnam 2025 is a single competition with 12 problems. Solving 11/12 is impressive but does not constitute a statistically robust demonstration that the efficiency gap is narrowing as a general trend — it is a single high-profile data point.
The 9-hour wall-clock time for Putnam 2025 used parallel computation across lemmas, meaning the actual total compute (H20-hours summed across all parallel workers) could be substantially higher than 9 hours. The paper reports a maximum budget of 40 H20-days per problem, which would mean up to 480 H20-days total across 12 problems if the budget were fully consumed. The 9-hour figure represents the makespan (wall-clock time from start to last solved problem), not the total computation.
The efficiency comparison with natural-language systems (e.g., DeepSeek-Math-V2's near-perfect Putnam 2024 performance) is qualitative, not quantitative. Natural-language systems report accuracy on competition problems; formal systems report verified proofs on a different set of competition problems. There is no common benchmark where both formal and natural-language provers are evaluated under comparable compute budgets.

The strongest evidence for the narrowing gap is the trajectory: AlphaProof 56% at 500 TPU-days/problem (2024), Seed-Prover 1.0 50% at 18 H20-days/problem, Seed-Prover 1.5 88% at 10 H20-days/problem (2025). If this trajectory continues, formal proving will soon match or exceed natural-language performance on the same benchmarks at comparable (or lower) cost. Seed-Prover 1.5 represents a significant step along this trajectory, but the extrapolation to "the gap is not intrinsic" requires assuming the trajectory will continue — an assumption the paper's evidence supports but does not prove.

6. Limitations and Trade-offs

Limitation 1: The Difficulty Estimation and Dataset Filtering Pipeline Is a Hidden Uncomputed Cost

The assumption or constraint. The post-training pipeline (Section 3.2) depends on a sophisticated filtering procedure to construct the RL training dataset. The SFT model is evaluated on each candidate problem under a light inference setting (Pass@4×8), and problems that the model proves more than three times are excluded, while problems that cannot be proved under any prompting strategy are also removed. The paper states: "We exclude any example that the model successfully proves more than three times, thereby focusing RL training on sufficiently challenging instances where additional learning signals are most beneficial." Additionally, the predicted difficulty estimation — required to bin problems for compute-optimal strategy selection — costs 2048 sample generations plus PRM scoring per problem, as acknowledged in the companion methodology.

The consequence. The filtering procedure itself consumes substantial compute that is never counted in the training or inference budgets. Every candidate problem in the training set must be evaluated under Pass@4×8 (up to 32 proof attempts per problem, each with tool interactions and Lean compilation) just to determine whether it qualifies for RL training. For the datasets mentioned — including "publicly available datasets and in-house formalized math textbooks including Graduate Texts in Mathematics" — this filtering cost could easily exceed the reported RL training budget. The consequence is that the paper's efficiency claims (10 H20-days per problem at inference, improvements over Seed-Prover 1.0's 18 H20-days) systematically undercount the total compute required to build the system. A practitioner attempting to replicate this pipeline would face substantial unstated costs in the data preparation phase that are not reflected in any of the paper's compute budgets or scaling curves.

What evidence exists in the paper. None. The paper does not report the size of the pre-filtering training set, the compute consumed by the filtering evaluation, or the fraction of candidate problems that survive filtering. There is no ablation comparing RL training on the filtered dataset versus an unfiltered (or differently filtered) dataset to quantify the benefit of the filtering procedure relative to its cost. The RL training dynamics (Figure 3a, 3b) show improvement over steps, but these curves begin after filtering and SFT cold-start — they do not account for the cost of getting to the starting point.

Mitigation status. Not addressed. The paper frames the filtering as a data quality step rather than a computational cost, and no future work is proposed to reduce or eliminate this overhead. A practitioner deploying a similar system would need to either replicate this expensive filtering pipeline (with unstated cost) or risk training on unfiltered data (with unknown impact on RL efficiency and final performance).

Limitation 2: The System Fundamentally Fails on Hard Problems Where the Base Model Lacks Core Capability

The assumption or constraint. The entire approach — agentic RL training, sketch-based decomposition, recursive test-time search — operates on the implicit assumption that the model's base capability is sufficient to eventually produce correct solutions given enough interaction and decomposition. The paper acknowledges this boundary explicitly in multiple places. On Erdős problems: "based on our observations, these problems are mathematically relatively simple, or we proved a trivial or simplified version of them due to mis-formalization." On the capability ceiling: "our systems, whether using natural language or formal language, are still some distance away from truly helping to advance research on frontier open mathematical problems." On Fate-X: the improvement from Seed-Prover 1.0 to 1.5 is only 9/100 to 10/100 for the agentic prover alone, with the full system reaching only 33/100.

The consequence. Test-time compute (recursive decomposition, more parallel attempts, deeper search) provides essentially zero return on problems outside the model's capability range. This is not a smooth degradation — it is a hard cliff. On Fate-X, even the full system with sketch-driven decomposition and 10 H20-days per problem solves only one-third of problems. On Erdős, the system only succeeds on problems that are "mathematically relatively simple" or where formalization errors accidentally made them easier. This means that for genuinely frontier mathematical research — the motivating application that justifies formal theorem proving's value proposition — the system provides no path forward. The paper's conclusion identifies a "critical dependency issue" in mathematical research (requiring synthesis across research papers, formalization of existing literature, and identification of relevant prior work), and acknowledges that the current system cannot address it. But the limitation is deeper than missing capabilities: it suggests that the RL + decomposition paradigm amplifies existing capability but does not create it, and for problems where the base model's pass@1 is near zero, no amount of test-time scaffolding helps.

What evidence exists in the paper. The Fate-X results (33% for full system, Table 2) and the Erdős qualitative assessment (Section 4.2) provide direct evidence of the capability ceiling. Figure 3b shows that RL training improves Putnam-200 performance monotonically, but this is within the model's capability range (the SFT model already solves a non-trivial fraction). The paper does not provide a difficulty-stratified breakdown showing that gains are concentrated in easier problems and vanish on harder ones — such an analysis would precisely characterize the capability boundary — but the Erdős discussion implies this pattern exists.

Mitigation status. The paper is unusually transparent about this limitation, particularly in the Erdős discussion and the conclusion. The conclusion explicitly identifies the "dependency issue" as an unsolved challenge and proposes future work on "identifying the most influential and relevant papers," "conducting natural language proofs grounded in these works," and "developing scalable approaches to formalizing both the papers themselves and the results derived from them." However, these are research program directions, not concrete mitigation strategies — the paper offers no evidence that the identified approach (formalizing dependency chains) is tractable with current or near-future methods.

Limitation 3: The Sketch Model's Reward Depends on an LLM-as-a-Judge Whose Reliability Is Unvalidated

The assumption or constraint. The sketch model is trained using rubric-based RL where the reward signal (Equation 2) depends critically on the $S_{\text{NL}}$ score — the natural language quality assessment produced by an LLM-as-a-Judge using the prompts in Appendix B. This judge is required to verify lemma correctness, detect mathematical falsehoods, identify missing hypotheses, and catch Lean-specific junk-value edge cases. The paper states: "We find using the natural language prover to disprove is cheaper than using a theorem prover" (Section 3.3), justifying the choice of LLM evaluation over formal verification for lemma quality.

The consequence. The sketch model is learning from a proxy reward that may have systematic errors. The LLM judge might: (a) approve mathematically false lemmas that it fails to recognize as false (false positives — the model gets rewarded for bad decompositions), (b) reject valid lemmas that it incorrectly identifies as flawed (false negatives — the model is penalized for good decompositions), or (c) exhibit systematic biases (e.g., favoring certain decomposition patterns that are not genuinely useful, or penalizing valid but unusual lemma structures). Any of these errors would propagate into the sketch model's training, potentially teaching it to produce decompositions that score well on the rubric but are suboptimal for the agentic prover. The paper provides no validation of the judge's accuracy against ground-truth formal verification — we do not know what fraction of lemmas the judge labels "correct" are actually provable in Lean, or what fraction it labels "incorrect" are actually unprovable. Without this calibration, we cannot assess whether the sketch model is learning genuine decomposition skill or merely learning to satisfy a fallible evaluator.

This is particularly concerning for the junk-value analysis component (Prompt 1 in Appendix B), which requires the judge to reason about subtle Lean 4 edge cases — divergent sums evaluating to 0, natural number subtraction returning 0, derivatives of non-differentiable functions returning 0. These are domain-specific technical details that general-purpose LLMs frequently mishandle. If the judge makes errors on junk-value cases (approving lemmas that are false in Lean despite being true in standard mathematics, or vice versa), the sketch model will learn decomposition strategies that are misaligned with what the Lean environment actually requires.

What evidence exists in the paper. None. The paper does not report the judge's accuracy, calibration, or agreement with human evaluators or formal verification. The rubric prompts (Appendix B) are presented as the evaluation methodology, but no validation experiment establishes that this methodology produces reliable rewards. The paper does not compare sketch models trained with rubric-based RL against sketch models trained with alternative reward sources (e.g., downstream agentic prover success rate as a proxy for decomposition quality). The system's strong overall performance (88% on PutnamBench) provides indirect evidence that the sketch model is producing useful decompositions, but this does not validate the judge's reliability — it is equally consistent with a scenario where the judge is noisy but the RL training is robust to noise, or where the sketch model's quality derives primarily from the SFT initialization and natural language prover's proof quality rather than from the RL training.

Mitigation status. Not addressed. The paper treats the rubric evaluation pipeline as validated by its careful design (detailed prompts, veto triggers, structured scoring dimensions) but does not empirically validate the pipeline's outputs. Future work on "developing more reliable semantic evaluators for decomposition quality" is not proposed, and the limitation is not acknowledged as a threat to validity. A practitioner adopting this methodology would need to independently validate the judge's reliability for their domain, which may require expensive formal verification of judge-labeled lemmas.

Limitation 4: The System Operates on a Single Benchmark Family and a Single Formal Language, With No Evidence of Cross-Domain Generalisation

The assumption or constraint. All experiments use the Lean 4 proof assistant and evaluate on competition-style mathematics benchmarks (PutnamBench, FATE, CombiBench, IMO, Putnam 2025, Erdős). The paper does not evaluate on non-competition formal mathematics (e.g., formalized research-level theorems from mathlib that are not competition problems), on other formal systems (Coq, Isabelle/HOL, Metamath), or on non-mathematical formal verification tasks (software verification, hardware verification, protocol verification). The model is trained on "a mixture of publicly available datasets and in-house formalized math textbooks including Graduate Texts in Mathematics" (Section 3.2), but these are all within the Lean/mathematics domain.

The consequence. We cannot determine whether the system's capabilities generalize beyond the specific combination of Lean 4 and competition-style mathematics. Several components are tightly coupled to Lean 4 specifically: the tool ecosystem (verify_lean via LooKeng, mathlib_semantic_search against a fixed mathlib4 commit), the RL reward (Lean compiler acceptance), the sketch model's structural verification (Lean type-checking), and the training data (Lean-formalized problems). The paper's title — "Mastering Undergraduate-Level Theorem Proving" — implies a broader capability than "solving PutnamBench problems in Lean," but the evaluation provides evidence only for the latter. A practitioner interested in formal verification of software systems using Coq, or in formalizing research-level algebraic geometry in Lean, would have no evidence that the methodology transfers.

The competition mathematics domain itself has specific characteristics that may not generalize: problems are self-contained (minimal dependency on external formalized libraries beyond mathlib), have known difficulty calibration (competition problem designers intend them to be solvable with specific techniques), and have clean correctness criteria (a single theorem statement to prove). The paper's conclusion identifies the "critical dependency issue" in research mathematics — the need to synthesize across multiple papers and formalize dependency chains — but this is not just a future challenge: it is a domain where the current methodology is untested and may fundamentally fail because the sketch model is trained on self-contained problems and has no mechanism for managing library dependencies.

What evidence exists in the paper. None beyond the stated benchmarks. The paper uses multiple benchmarks within the competition-mathematics domain (Putnam, FATE, CombiBench, IMO, Erdős) and across different difficulty levels (undergraduate, graduate, PhD), which provides some evidence of within-domain generalization. But all evaluations use Lean 4, all involve self-contained theorem-proving tasks, and the Fate-X results (33%) suggest that generalization degrades at the PhD level — which is precisely where cross-domain transfer would be most needed for research applications.

Mitigation status. Not addressed as a limitation. The paper frames its contribution in terms of formal theorem proving in Lean specifically, but the broader claims about "mastering undergraduate-level theorem proving" and "narrowing the gap with natural language reasoning" imply generality that is not tested. No future work is proposed on cross-system or cross-domain transfer. The release of model weights and code (the project page) enables independent evaluation on other benchmarks, but the paper itself provides no evidence of generalisability.

Limitation 5: The Pass@k×m Budget Allocation Strategy Is Never Justified or Optimised, and Its Sensitivity Is Unexplored

The assumption or constraint. The paper uses specific Pass@k×m budget allocations throughout the experimental pipeline without justification or ablation: Pass@4×8 for the SFT filtering evaluation (Section 3.2), Pass@8×8 for the standalone agentic prover evaluation (Table 1), and Pass@3×3 for the agentic prover within the test-time workflow (Section 3.4). These choices determine the balance between parallel exploration (k independent trajectories) and sequential refinement (m summarisation-based retries per trajectory). The tradeoff is non-trivial: parallel exploration is better for problems where the model has a reasonable chance of producing a correct proof on any single attempt (more independent samples increase the probability of hitting a correct one), while sequential refinement is better for problems where the model's first attempt is usually wrong but contains useful partial progress that can be improved through summarisation and retry. The optimal allocation likely depends on problem difficulty — easy problems benefit from more parallelism, hard problems from more sequential refinement with learning from failures.

The consequence. The paper's reported performance numbers are specific to budget allocations that were chosen without documented optimisation. Different allocations might yield substantially different performance: Pass@2×12 (fewer independent trajectories, more retries per trajectory) might outperform Pass@8×3 (more trajectories, fewer retries) on Fate-X problems where initial attempts are almost always wrong but partial progress enables recovery; Pass@16×2 might outperform Pass@4×8 on easy PutnamBench problems where the model is likely to succeed on any given attempt. Without knowing the sensitivity of performance to the k×m split, we cannot determine whether the reported numbers represent optimal allocation or an arbitrary choice that happens to work adequately.

This limitation also affects the compute budget comparisons. When the paper claims Seed-Prover 1.5 uses 10 H20-days per problem versus Seed-Prover 1.0's 18 H20-days, the comparison assumes both systems are running at their respective optimal budget allocations. If Seed-Prover 1.5's Pass@3×3 within the test-time workflow is suboptimally tuned, its compute efficiency might be understated (it could achieve the same performance with less compute using a different allocation). Conversely, if Seed-Prover 1.0's medium workflow budget was suboptimally tuned, the efficiency comparison overstates Seed-Prover 1.5's advantage.

What evidence exists in the paper. None. The paper never varies the k×m split, never reports performance at different allocations, and never discusses the parallel-vs-sequential exploration tradeoff. The test-time scaling analysis (Figure 6a) varies total compute budget but keeps the allocation strategy fixed, so we learn how performance scales with more total compute but not whether different allocations of that compute would scale differently. The compute-optimal test-time compute scaling literature (referenced in the prior sections but not by this paper) has established that optimal allocation between parallel and sequential strategies is difficulty-dependent — this paper does not engage with that finding or its implications for formal theorem proving.

Mitigation status. Not addressed. The paper does not acknowledge the allocation strategy as a design choice requiring justification, does not propose future work on optimising budget allocation, and does not discuss the parallel-vs-sequential tradeoff in any section. A practitioner deploying this system would need to conduct their own allocation sensitivity analysis, which would require substantial additional computation (evaluating multiple k×m combinations per benchmark).

Limitation 6: The Sketch Model and Agentic Prover Are Trained and Evaluated on the Same Model Family With No Diversity Analysis

The assumption or constraint. The entire pipeline depends on specific model initialisations: the agentic prover is post-trained from Seed-Prover 1.0, and the Natural Language Prover is initialised from Doubao-Seed-1.6. The paper does not experiment with different base model families, sizes, or pretraining distributions. The sketch model's architecture is not described (parameter count, pretraining data, relationship to the agentic prover's base model). The paper evaluates only one model checkpoint per component (the 1055th-step RL checkpoint for the agentic prover, an unstated checkpoint for the sketch model).

The consequence. We cannot determine whether the system's performance derives from the training methodology (agentic RL, rubric-based sketch training, recursive test-time workflow) or from the specific base models used. If the gains are primarily due to the capabilities of Doubao-Seed-1.6 (for natural-language reasoning) and Seed-Prover 1.0 (for formal proving), then the methodology might not transfer to weaker base models — and the contributions would be narrower than claimed. Conversely, if the methodology is robust to base model quality, it might produce even larger gains when applied to stronger base models — but we have no evidence either way.

This limitation is particularly acute for the sketch model. The paper presents rubric-based RL as a general training methodology for proof decomposition, but evaluates it only with one base model (which is not described) and one natural-language prover (Doubao-Seed-1.6). If Doubao-Seed-1.6 produces unusually high-quality natural-language proofs that make the sketch model's task easier, the rubric RL might add little value over a simpler SFT baseline — the sketch model might be learning to predictably decompose high-quality inputs rather than learning a robust decomposition skill that works with variable-quality proofs. The paper provides no evidence that the sketch model trained with rubric RL outperforms a sketch model trained with simpler methods (SFT, Lean-only structural reward) when both are evaluated with the same natural-language prover.

Finally, the single-checkpoint evaluation means we have no measure of training stability or variance. The 1055th-step checkpoint was selected based on Putnam-200 performance; we do not know how nearby checkpoints (e.g., step 1000, step 1100) perform, whether performance is stable across checkpoints or spiky, or whether the reported numbers are representative of the training run or unusually favourable. For a paper making strong quantitative claims (88% on PutnamBench, 11/12 Putnam 2025 in 9 hours), this lack of variance information makes it difficult to assess whether the results are reproducible or contingent on a specific lucky training run.

What evidence exists in the paper. None that addresses model diversity or training stability. The paper reports results from a single training run with a single base model family, evaluated at a single checkpoint. There are no experiments varying model size, pretraining distribution, or architecture. There are no error bars, confidence intervals, or multi-seed analyses.

Mitigation status. Not addressed. The paper does not acknowledge base model dependence as a limitation, does not discuss model diversity as a dimension for future work, and does not provide multiple training seeds to assess stability. The release of model weights (via the project page) partially mitigates this by enabling independent evaluation on different base models, but the paper itself provides no evidence of methodological robustness.

7. Implications and Future Directions

How This Work Changes the Landscape

This paper shifts the formal theorem proving field from a paradigm of fixed interaction protocols toward learned interaction strategies, where the model — not the system designer — determines how and when to engage with the proof assistant. Prior work operated within a dichotomy that the field had implicitly accepted as exhaustive: either interact with Lean at every tactic (step-level provers like AlphaProof and Aristotle) or interact once with a complete proof (whole-proof provers like DeepSeek-Prover-V2 and Seed-Prover 1.0). Seed-Prover 1.5's agentic prover breaks this dichotomy by operating at a dynamically chosen lemma granularity and learning through extensive RL what interaction frequency, tool-use pattern, and caching strategy is effective for different types of problems. The evidence that this learning occurs is not speculative — it is documented in the training dynamics. Figure 4a shows tool calls dropping from ~15 to ~10 per trajectory while success rate nearly doubles (Figure 3a). Figure 5 shows search calls decreasing while performance improves, demonstrating that the model internalizes knowledge previously accessed through retrieval. These are emergent behaviors that no system designer programmed; they emerged because the RL objective (binary outcome reward with a negative penalty for failure) created pressure for the model to discover efficient interaction strategies on its own.

The methodological significance extends beyond theorem proving. The paper demonstrates that sparse, delayed, binary rewards — exactly the kind that formal verification environments naturally provide — are sufficient to drive complex behavioral change in tool-use agents, provided the training data is curated to focus on challenging-but-provable instances. This is a non-trivial finding. The conventional wisdom in RL for reasoning has been that sparse rewards require careful shaping or dense intermediate signals to support credit assignment. Seed-Prover 1.5's training succeeds with a pure outcome reward (+1 for a verified proof, −1 otherwise), suggesting that the combination of a well-structured action space (tool calls with clear effects) and a curriculum of appropriately difficult problems can overcome the credit assignment challenge without hand-crafted shaping. This has implications for any domain where ground-truth verification exists but is sparse — software verification, hardware design, logistics planning, or any task where correctness can be checked mechanically at the end but not incrementally.

Resolving prior contradictions. The paper reconciles a tension that has been building in the formal theorem proving community. On one side, systems like AlphaProof demonstrated that RL in formal environments could produce olympiad-level results, but at enormous computational cost (500 TPU-days per problem) that made the approach seem impractical. On the other side, systems like Hilbert and Aleph achieved competitive performance without massive compute but relied on extensive test-time search (thousands of attempts per problem) rather than training-time learning, suggesting that RL might not be necessary. Seed-Prover 1.5 resolves this tension by showing that RL is highly effective when applied to the right interaction paradigm — agentic lemma-level proving rather than step-level tactic generation. The compute efficiency gains (10 H20-days per problem vs. AlphaProof's 500 TPU-days) are not because RL was abandoned or replaced with search; they are because the RL-trained model learns to use its inference budget more strategically. The lesson is not "RL doesn't work for formal proving" or "RL is the only way" — it is that the interaction paradigm matters more than the training algorithm, and the right paradigm enables RL to be both effective and efficient.

Shifting research priorities. The paper's findings redirect attention in several ways. First, verifier design becomes less central to the formal proving agenda. In natural-language reasoning, a major focus has been training reliable verifiers (process reward models, outcome reward models) to guide search and select solutions. In formal proving, Lean is the verifier — it provides an objective, non-gameable correctness signal. The challenge shifts from building verifiers to building systems that can effectively use the verification signal that already exists. This means the formal theorem proving community should focus on interaction design and training methodology (how to structure the agent's action space, reward, and curriculum) rather than on verifier engineering.

Second, test-time search becomes a complement to training, not a substitute. Prior systems like Hilbert and Aleph achieved strong results through extensive test-time search (thousands of attempts per problem). Seed-Prover 1.5 shows that investing compute in RL training produces a model that requires less test-time search — the 10 H20-day budget includes both the learned decomposition and the proving attempts, and the majority of PutnamBench problems are solved within the first few hours (Figure 6b). This suggests a reallocation of compute budgets: rather than spending 500 TPU-days per problem on inference-time search, invest in training a more capable agentic prover that solves most problems with modest inference budgets, reserving test-time compute for the long tail of genuinely hard problems.

Third, natural-language reasoning becomes an asset rather than a competitor to formal proving. The paper's opening question — whether formal proving is still worth pursuing given strong natural-language results — is answered not by arguing that formal is inherently better, but by demonstrating that natural-language reasoning can accelerate formal proving through the sketch model's learned decomposition. This is a genuine reframing: rather than formal and natural-language proving competing for the same resources, they become complementary components of a single system. The natural-language prover provides high-level proof strategy; the sketch model translates this into formal structure; the agentic prover handles low-level formal details. This symbiosis is what enables the system to solve 88% of PutnamBench — a result that neither component could achieve alone.

Follow-Up Research This Work Enables

Verifying the internalization hypothesis with problem-level tracking. Figure 5 shows that search calls decrease while performance improves across RL training, which the paper interprets as the model "internalizing knowledge from search results." This is a specific, testable hypothesis: the model learns to retrieve mathlib theorems from its parameters rather than through explicit search. A direct follow-up would instrument the training run to track, for each individual problem, the number of search calls and the specific theorems retrieved at each training step. If internalization is occurring, the same problem that required 15 search calls at step 200 should require 3 search calls at step 1000, with the model directly invoking the previously-searched theorems without querying mathlib. A strong result would show that theorem recall accuracy (the fraction of needed theorems the model retrieves from parameters rather than search) increases monotonically with training steps, and that internalization precedes performance improvements (the model first learns the theorems, then learns to use them effectively). A negative result — search calls decrease because the model stops attempting hard problems that require search — would refine our understanding of what RL is actually teaching and would motivate different training curricula that prevent the model from avoiding hard problems.

Ablating the sketch model's rubric RL against simpler reward designs. The sketch model is trained with an elaborate rubric-based LLM-as-a-Judge (Appendix B) that evaluates lemma correctness, decomposition quality, and junk-value edge cases. The paper provides no evidence that this complex reward design produces better sketches than simpler alternatives. A direct ablation study would train sketch models using: (a) the full rubric RL as in the paper, (b) a binary reward based only on Lean structural verification (does the sketch compile modulo sorry-filled lemmas?), (c) a scalar LLM judge that outputs a single quality score without the structured rubric, (d) a reward based on downstream agentic prover success (reward sketches whose lemmas the agentic prover can actually prove), and (e) SFT only on ground-truth human-written decompositions. Evaluate all variants on PutnamBench using the same agentic prover and test-time workflow. The critical measurement is whether the rubric's sophisticated checks (veto triggers, lemma-by-lemma verification, tier-based decomposition scoring) produce measurable improvements over a simple "does the sketch compile?" reward that is essentially free to compute. If the complex rubric adds little over the Lean-only reward, the field can dispense with expensive LLM evaluation for sketch training. If the rubric provides substantial gains, the specific components that matter (lemma verification vs. alignment scoring vs. junk-value checking) should be identified.

Measuring the agentic prover's generalisation to non-competition formal mathematics. All evaluation is on competition-style problems (Putnam, FATE, IMO, CombiBench) that are self-contained and designed to be solvable with undergraduate/graduate techniques. A critical unanswered question is whether the agentic prover's learned interaction strategies transfer to the kind of formal mathematics that appears in mathlib contributions — formalizing research papers, building theory libraries, or proving lemmas in ongoing formalization projects. A concrete experiment would evaluate the agentic prover on a held-out set of recently merged mathlib PRs that required non-trivial proofs, stratified by proof length and dependency depth. The agentic prover could be evaluated in two modes: (a) direct application (can it prove the target lemma given access to the relevant mathlib context?), and (b) library-extension mode (can it prove lemmas that depend on recently formalized definitions not well-represented in its training data?). The prediction from the paper's findings is that the agentic prover's efficiency gains (fewer tool calls, shorter sequences, internalized theorem knowledge) will transfer, but its capability ceiling will be lower on research-level mathematics than on competition problems because the training data overrepresents self-contained competition-style problems. A strong positive result — the agentic prover generalises well to library formalization tasks — would dramatically expand the system's practical applicability beyond benchmarks.

Stress-testing the recursive decomposition depth against problem complexity. The test-time workflow's recursive decomposition (natural language proof → sketch → agentic proving, with up to depth-8 search via restart) is the mechanism that converts the sketch model and agentic prover into a complete system. But we do not know how this depth interacts with problem complexity. A systematic stress test would take a set of PutnamBench problems, measure their "decomposition depth" (the minimum number of recursive decompositions needed to break them into agentic-provable lemmas), and correlate this with the system's success rate and compute cost. The hypothesis is that problems requiring deeper decomposition (more levels of lemma nesting) are disproportionately harder and consume disproportionately more compute, potentially explaining the heavy tail in Figure 6b. A strong result would identify a depth threshold beyond which the system's success rate drops sharply — a "decomposition cliff" that defines the practical limits of the approach. If such a cliff exists, it would motivate research on better decomposition strategies (perhaps training the sketch model explicitly on deeply nested decompositions) rather than simply scaling compute. If no cliff exists (success degrades smoothly with required depth), it would validate the recursive approach as robust and suggest that further scaling of depth and compute will continue to yield improvements.

Applying agentic RL with outcome rewards to other formal systems. The paper's training methodology — VAPO-based RL with binary outcome rewards in a tool-use environment with ground-truth formal verification — should transfer to any formal verification system that provides a binary accept/reject signal. Concrete targets include Coq (widely used for software verification and programming language theory), Isabelle/HOL (used for hardware verification and mathematical formalization), and Dafny or Verus (for program verification). A transfer experiment would take the same agent architecture (LLM with tools for verification, library search, and auxiliary computation), adapt the tools to the target system's APIs (Coq's coqc, Isabelle's isabelle), construct a training set of formalized problems from that system's standard libraries and benchmark suites, and apply the same SFT + RL pipeline. The key measurements are: (a) whether the RL training dynamics show similar patterns (improving accuracy, decreasing tool calls, internalization of library knowledge), and (b) how much the methodology's effectiveness depends on the specific tools and verification feedback provided (Lean's error messages are notoriously inscrutable; other systems may provide more or less informative feedback, affecting credit assignment). A strong positive result — the methodology transfers with minimal modification — would establish agentic RL as a general approach to formal verification, not a Lean-specific technique.

Evaluating whether the sketch model learns genuine mathematical decomposition or pattern matching. The sketch model's rubric-based training rewards it for producing decompositions that an LLM judge deems mathematically valid and structurally sound. But we do not know whether the model is learning a genuine understanding of mathematical decomposition (identifying sub-goals that genuinely simplify the problem) or pattern-matching against superficial features of its training data (producing lemmas that "look like" decompositions but do not meaningfully reduce difficulty). A diagnostic experiment would evaluate the sketch model on problems from PutnamBench that are isomorphic to training problems in structure but use different mathematical domains — e.g., a number theory problem decomposed using the same lemma structure as an algebra problem from the training set. If the sketch model produces structurally similar decompositions that are mathematically appropriate for the new domain, it suggests genuine decompositional reasoning. If it produces lemmas that mirror training patterns but are mathematically nonsensical for the new domain (e.g., using algebra-specific lemmas in a topology problem), it suggests pattern matching. A companion experiment would measure the "difficulty reduction ratio" — the fraction of problems where the agentic prover's success rate on individual lemmas is higher than its success rate on the original theorem — for in-distribution vs. out-of-distribution problems. Genuine decomposition should maintain a high difficulty reduction ratio even on out-of-distribution problems; pattern matching would show a sharp drop.

Practical Applications and Downstream Use Cases

Automated formalization of competition mathematics as a training data pipeline. The system's ability to solve 11/12 Putnam 2025 problems within 9 hours (Table 4) makes it practical to run Seed-Prover 1.5 on entire competition archives — not just for benchmarking, but to generate large-scale verified formal proof data. For each solved problem, the system produces a complete, compiler-verified Lean proof with explicit lemma structure. This data can be used to train stronger provers (via distillation, SFT on the generated proofs, or as additional RL training data), to augment mathlib with formalized competition mathematics, or to create benchmarks for evaluating future systems. The 88% solve rate on PutnamBench (580/660 problems) means the system could contribute hundreds of new verified proofs to the Lean ecosystem at a compute cost of ~10 H20-days per solved problem. This is a concrete, immediately actionable use case: run Seed-Prover 1.5 on the remaining unsolved PutnamBench problems (and on other competition benchmarks like IMO Shortlist or national olympiads), curate the verified proofs, and release them as a public dataset to accelerate the entire field's progress.

Undergraduate/graduate mathematics education with verified feedback. The system's performance on Fate-H (80%, graduate-level) and PutnamBench (88%, undergraduate-level) makes it technically viable as an automated tutoring tool for formal mathematics. A student working on a problem set in, say, abstract algebra or real analysis could submit their problem to Seed-Prover 1.5 and receive not just a binary "provable/unprovable" verdict but a structured formal proof (lemma decomposition + verified Lean code) that demonstrates one correct approach. The system solves the majority of problems at these levels within hours (Figure 6b shows most PutnamBench solves in the first few hours), making it responsive enough for interactive use. The key practical concern is the compute cost: at 10 H20-days per problem for the full budget, running the system on every student problem would be expensive. But the paper's results suggest that most problems are solved with much less compute (Figure 6a shows ~300 solves at 1 H20-day/problem), and a budget-capped deployment (e.g., 1 H20-hour per problem, aborting if unsolved) could handle the majority of undergraduate-level problems at reasonable cost while escalating only the hardest problems to more expensive computation.

Batch verification of mathematical competition solutions. Organisations that run mathematical competitions (the Putnam committee, national olympiad committees, the IMO) face the challenge of verifying thousands of student-submitted solutions for correctness. Currently, this is done by human graders — a slow, expensive, and error-prone process. Seed-Prover 1.5's capability on competition mathematics suggests a pipeline where (1) human experts formalize the problem statements in Lean (a one-time cost per competition), (2) student solutions are translated into formal proof sketches (potentially using the sketch model or a simpler formalization model), and (3) the system discharges the lemma obligations to verify correctness. The 88% solve rate on PutnamBench is not high enough for fully automated grading (12% of correct solutions would be incorrectly marked as unproven), but the system could serve as a pre-filter: solutions that the system verifies are guaranteed correct (Lean compilation is sound), allowing human graders to focus their attention on the subset of solutions the system cannot verify, which includes both genuinely incorrect solutions and correct solutions beyond the system's current capability. This would reduce grading workload by up to 88% for undergraduate-level competitions while maintaining the trustworthiness of formal verification for the automated portion.

Self-improving formal mathematics libraries via iterative RL. The paper's training pipeline — filtering problems by SFT solvability, RL training on challenging-but-provable instances, checkpoint selection, and deployment — can be applied iteratively. After one round of RL training produces a stronger prover (the step-1055 checkpoint), that prover can be used to generate verified proofs for problems that the previous model could not solve. These newly solved problems become training data for the next RL round, potentially expanding the model's capability frontier. This is the "iteratively leveraging the RL-trained model to collect additional data" that the paper mentions as future work (Section 3.2). The critical practical question is whether the capability gains compound or saturate. The paper's evidence — 50% → 90% training accuracy in one RL round, 50% → 88% on PutnamBench across the full pipeline — suggests substantial headroom remains before saturation. An iterative deployment would: (a) run the current system on a large corpus of formalized problems (not just benchmarks, but newly formalized textbook exercises, mathlib contributions, and competition problems), (b) collect all successful proofs as new training data, (c) re-train the agentic prover on the expanded dataset, (d) evaluate on held-out benchmarks, and (e) repeat. This creates a virtuous cycle where each iteration expands the model's training distribution with verified proofs it discovered itself, potentially bootstrapping from undergraduate-level capability toward graduate-level and beyond without requiring human formalization effort.

Dependency tree

Papers this one builds on, walking backwards through the same domain and shared topics.

SAGE: Training Smart Any-Horizon Agents for Long Video Reasoning with Reinforcement Learning2025· agents← in-domain predecessor
- Scaling RL to Long Videos2025· rl-training← LLM-judged similar
- Memory in the Age of AI Agents2025· agents← in-domain predecessor
- CUA-Gym: Scaling Verifiable Training Environments and Tasks for Computer-Use Agents2026· agents← similar topic
- Demystifying Reinforcement Learning in Agentic Reasoning2025· agents← similar topic
- Reflexion: Language Agents with Verbal Reinforcement Learning2023· agents← similar topic
Scaling Agent Learning via Experience Synthesis2025· agents← similar topic
- Scaling Generalist Data-Analytic Agents2025· agents← LLM-judged similar
- AgentFrontier: Expanding the Capability Frontier of LLM Agents with ZPD-Guided Data Synthesis2025· data← LLM-judged similar
- The Collaboration Gap2025· agents← in-domain predecessor
- ScaleEnv: Scaling Environment Synthesis from Scratch for Generalist Interactive Tool-Use Agent Training2026· agents← similar topic
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving2019· agents← similar topic
- Realization of the anisotropic XY model in a Tb(III)-W(V) chain compound2012· agents← in-domain predecessor

What it influenced

Later papers in the same chain. Direction reversed.

MAI-UI Technical Report: Real-World Centric Foundation GUI Agents2025· agents→ in-domain predecessor
- Confucius Code Agent: Scalable Agent Scaffolding for Real-World Codebases2025· code→ LLM-judged similar
- KernelEvolve: Scaling Agentic Kernel Coding for Heterogeneous AI Accelerators at Meta2025· agents→ in-domain predecessor
- AutoRT: Embodied Foundation Models for Large Scale Orchestration of Robotic Agents2024· agents→ similar topic
- UI-TARS-2 Technical Report: Advancing GUI Agent with Multi-Turn Reinforcement Learning2025· agents→ similar topic
- Game-TARS: Pretrained Foundation Models for Scalable Generalist Multimodal Game Agents2025· agents→ similar topic
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving2019· agents→ similar topic
- How Does NLP Benefit Legal System: A Summary of Legal Artificial Intelligence2020· agents→ in-domain predecessor
Agent Learning via Early Experience2025· agents→ similar topic
- Demystifying Reinforcement Learning in Agentic Reasoning2025· agents→ in-domain predecessor
- Scaling Agent Learning via Experience Synthesis2025· agents→ similar topic