Suppose a model fails to prove a theorem, but establishes two useful lemmas along the way. A second attempt can start from the original statement, or it can start with those lemmas already available. In the latter case, the system has made progress even though the attempt failed. Its context can be reset without discarding everything it learned.
This is the relevant distinction when an AI system spends hours or days on a mathematical problem. The run need not be one exceptionally long chain of thought. It can consist of many model calls, proof attempts, compiler interactions, and revisions, with selected results carried between them. Seed-Prover and AlphaProof Nexus provide concrete examples (J. Chen et al. 2025; Tsoukalas et al. 2026).
Understanding these systems requires separating three questions: what can be checked, what survives an attempt, and how the next attempt is chosen. A proof checker helps with the first. It does not, by itself, answer the other two.
From a trained policy to a search system
The standard pretraining and assistant post-training pipeline produces a policy: a distribution over responses given an input (Ouyang et al. 2022). Reasoning post-training changes that distribution; a long-running system must additionally decide how to invoke the policy, evaluate its outputs, and retain useful work.
A common training method is reinforcement learning with verifiable rewards (RLVR). Given a prompt \(x\), sample completions \(y_1,\ldots,y_G \sim \pi_\theta(\cdot\mid x)\), score them, and update the policy to favour higher-reward completions. GRPO uses rewards relative to the other samples for the same prompt to estimate advantages, avoiding a separately trained value network (Shao et al. 2024). For the present discussion, the important choice is not the policy-gradient estimator but the source of the reward.
A program can compare a final answer with a reference, run a test suite, or check syntactic constraints. Such checks also apply outside mathematics: to SQL outputs, formatting requirements, or valid tool calls. Where no adequate programmatic check exists, the scorer might instead be a learned preference model, an LLM applying a rubric (Gunjal et al. 2025), or agreement among sampled answers. These signals have different failure modes. Optimisation can exploit a learned scorer’s errors, but a deterministic checker can also reward the wrong thing: passing a thin test suite is not general program correctness, and matching a final answer does not validate the derivation.
It is also necessary to distinguish a training reward from a deployment-time verifier. A reference-answer matcher is useful during training but unavailable for a new question whose answer is unknown. A formal proof checker is different: it needs the statement and a proposed proof, not a previously known answer. It can therefore remain in the loop during deployment.
DeepSeek-R1’s exclusion of mathematical proofs illustrates the first limitation, not a limitation of RLVR in principle. Its reasoning rewards relied on checkable outcomes, and the authors excluded proofs because they could not reliably judge their correctness. They also avoided neural outcome and process reward models for reasoning because of reward hacking (Guo et al. 2025). This establishes the scope of that training setup. It does not establish that intermediate feedback is unnecessary, or that proof-based rewards are unavailable once proofs are represented formally.
What verification does—and does not—provide
Write \(V(g,a)\) for a verifier applied to a goal \(g\) and an artifact \(a\). Its guarantee depends on what it checks. An answer matcher checks agreement with a reference. A test suite checks the tested behaviours. Lean is a proof assistant whose small trusted core—the kernel—checks that a proof term establishes a formal statement under the permitted axioms. Only the last is a proof certificate, and even then the formal statement must faithfully express the intended mathematics.
For reasoning about incomplete work, it is useful to distinguish acceptance, rejection, and no certificate yet: \(V(g,a)\in\{1,0,\bot\}\). This is an abstraction, not Lean’s literal interface. In particular, rejection of a proposed proof is not a disproof of its theorem, and exhaustion of a search budget is not evidence that the theorem is false.
A decomposition \(D\) proposes subgoals \(g_1,\ldots,g_m\) together with an argument that establishes \(g\) once they are proved. The connecting argument matters: a list of plausible lemmas is not yet a decomposition of the original problem.
Consider a Lean file containing six auxiliary lemmas and a main proof that combines them. Each lemma’s unfinished proof is represented by sorry. Lean can accept such a file because sorry admits the missing propositions. That checks the structure of the argument conditional on those admissions; it does not establish the six lemmas. A successful proof must discharge the relevant holes without changing the target or introducing unapproved assumptions (J. Chen et al. 2025; Tsoukalas et al. 2026).
There are consequently two different questions about this sketch. Does the target follow from the proposed lemmas? The formal system can check that. Are the lemmas true, tractable, and a useful way to divide the work? An unfinished sketch does not answer those questions. A decomposition can be logically sufficient yet computationally unhelpful—for example, by putting almost the entire original problem into one auxiliary lemma.
This is where heuristic guidance enters. Let \(\widetilde V\) denote a score used to rank candidates or estimate the usefulness of unfinished work. It might come from a value model, a rubric-based judge, or a vote. A system need not implement it as a separate network: the policy’s decision to pursue one approach rather than another is already a heuristic choice. What it cannot obtain from the proof checker alone is an estimate of the expected progress per unit of compute.
The limitation is therefore narrower than “verification only works at the end.” A checker can validate a completed lemma long before the target theorem is proved, and it can constrain intermediate proof states. What it does not generally supply is a search policy.
What survives an attempt
Call the retained state \(\Sigma\). Independent sampling retains candidates for selection but does not let later generations learn from earlier attempts. A single long trajectory does condition on its previous reasoning, but only while that reasoning remains available in context. An external file, proof-state database, or lemma store allows a fresh context to continue the same search. Updating the weights changes the policy itself.
These forms of persistence determine what can be carried forward, not how long continued work will be useful. That also depends on model capability, context use, tool cost, parallelism, and search decisions. Persistence makes continuation possible; it does not guarantee progress.
The more important distinction is between a saved conjecture and a saved result. Notes about a failed approach can be useful, but they can also preserve mistakes. A verified lemma can be reused without trusting the trajectory that discovered it, provided its statement, dependencies, and assumptions are preserved. Seed-Prover makes this explicit by extracting local have blocks into top-level lemma declarations that later attempts can access (L. Chen et al. 2025).
The statements of retained lemmas still have to fit the remaining argument. Verification guarantees their correctness under stated assumptions, not their usefulness. Informal notes can guide the search too, but without the same guarantee.
A stateful proof-search loop can therefore look like this:
while budget remains and the target is unresolved:
choose a goal and retrieve relevant saved work
propose a proof, a decomposition, or a revision
check completed proofs and the structure of new sketches
retain verified results; record other feedback separately
update the search state and allocate the next attemptThe policy proposes work, the verifier checks specified properties, the store preserves results, and the controller chooses what happens next. A heuristic scorer may assist that controller. Context resets occur inside this loop rather than terminating it.
Coverage is not selection accuracy
Even without decomposition, additional compute poses an evaluation problem. Generating a correct candidate somewhere in a large sample is different from returning it.
For a fixed goal, draw \(k\) candidates independently from the same policy. Define their coverage as
\[ c(k)=\Pr\!\left[\exists i\leq k:\ V(g,a_i)=1\right], \]
and let \(s(k)\) be the probability that the candidate selected from that same pool is correct. Averaging both quantities over the same problem distribution gives the corresponding benchmark measures. Their difference,
\[ \Gamma(k)=c(k)-s(k), \tag{1}\]
is the selection gap. An ideal verifier could recover the covered solutions, ignoring verification cost; a heuristic selector may not.
For Llama-3-8B-Instruct on a 128-problem MATH subset, increasing the sample count from 100 to 10,000 raised coverage from \(82.9\%\) to \(98.44\%\), while the best improvement from the tested selection methods was only \(40.50\%\) to \(41.41\%\) (Brown et al. 2024). At 10,000 samples, the gap was about 57 percentage points. These experiments show a substantial selection bottleneck for those models and selectors, not that repeated sampling is intrinsically ineffective.
The distinction also explains why a neural verifier can be useful without being reliable enough to certify a proof. Selection requires a good ordering within a candidate set. Certification requires controlling false acceptance. A scorer can rank well despite poor calibration; that does not make its highest-scoring candidate trustworthy. Conversely, even modest ranking errors can be costly when correct candidates are rare.
Mahdavi et al. (2025) combine pairwise generative selection with repeated LLM judgements. On Challenge-19, the resulting system raises final-answer accuracy from a single-sample baseline of \(47.07\%\) to \(96.05\%\). The scope and cost are important: these are nineteen integer-answer problems selected to have nonzero but below-70% solve rates, not a broad proof-certification benchmark. The best configuration uses 1,008 model calls per problem: 256 for candidate generation and 752 for selection and judging. The reported accuracy is averaged across eight seeds.
In a separate verifier-training experiment, proof-level \(F_1\) rises from \(37.23\) to \(68.75\), but final-answer precision moves only from \(60.41\%\) to \(62.59\%\), within the reported variability, while recall falls from \(67.43\%\) to \(17.18\%\). The verifier becomes much more selective without a demonstrated improvement in the correctness of accepted answers. This is consistent with the authors’ concern that proof-grading metrics can reward stylistic or procedural features; it does not identify that mechanism conclusively. Another experiment accepted seven of 48 critically flawed proofs, illustrating the remaining false-acceptance problem.1
For a system whose output will receive expert review, a good ranker can substantially reduce the review burden. A system required to produce a machine-checkable certificate needs a suitable formal verifier as well. Ranking and certification are complementary components, not interchangeable ones.
Five ways to spend additional compute
The following designs differ in what they do between policy calls. They are not mutually exclusive: a file-editing agent can decompose a goal, a recursive prover can sample many candidates per lemma, and either can update its policy.
| Design | Unit of work | Retained state \(\Sigma\) | Guidance |
|---|---|---|---|
| Long trajectory | One extended response | Current context | Policy-internal planning and correction |
| Sample and select | Whole candidate | Candidate pool | Hard verifier, learned ranker, or vote |
| Recursive formal decomposition | Lemma or subgoal | Checked lemmas and search state | Kernel feedback and sketch heuristics |
| File-based agent | Edit or tool interaction | File and episode summaries | Compiler feedback and policy; optional critic |
| Test-time adaptation | Training update | Weights, optionally alongside explicit state | Verified or estimated rewards |
Search within one trajectory
R1, Kimi k1.5, and s1 all use long trajectories in which planning, backtracking, and correction are expressed in tokens (Guo et al. 2025; Team et al. 2025; Muennighoff et al. 2025). The training routes differ. R1 and Kimi use reinforcement learning; s1 uses supervised distillation from a reasoning model and a decoding intervention that can append “Wait” when the model tries to stop. They should not be treated as instances of one training algorithm.
The attraction is architectural simplicity. Much of the search is delegated to the policy, without an external tree of partial solutions or an explicit intermediate-step scorer. Kimi shows that strong performance is attainable without tree search, value functions, or process reward models. It does not show that those additions would be unhelpful: the paper does not ablate them. Its strongest Codeforces result also uses an outer selection procedure over generated programs and model-generated tests. That is compatible with avoiding tree search within a trajectory, but it is not a search-free inference system.
The limitation of the pure version is its state: once a trajectory is discarded, later independent attempts cannot reuse its intermediate discoveries. External summaries or tools can change that, but then the system has acquired another component. Longer responses alone are also an unreliable proxy for improvement; both R1’s length curve and s1’s budget-forcing results require qualifications.2
Sampling whole solutions
Independent sampling is easy to parallelise. With a hard deployment-time verifier, the system can stop when a valid candidate is found. Without one, its usable performance depends on the selection gap in Equation 1.
Sampling also depends on the generator assigning enough probability to a successful attempt. Brown and coauthors report zero observed coverage on CodeContests for all eight tested Pythia models even at 10,000 samples (Brown et al. 2024). This is evidence that sampling was insufficient at that budget, not proof that the success probability was exactly zero.
DeepSeek-Prover-V2 illustrates why training and inference architectures must be described separately. Its subgoal decomposition is used during training to construct verified reasoning data. The large model’s reported inference procedure is independent whole-proof sampling, rather than an adaptive decomposition search (Ren et al. 2025). It therefore belongs in this category at deployment, despite decomposition being central to how it was trained.3
The absence of reuse is the other cost. Finding a useful lemma in one failed candidate does not help another unless the system explicitly extracts it and conditions subsequent attempts on it.
Recursive decomposition with a proof checker
A recursive prover makes that reuse part of the algorithm. It proposes a proof sketch, attempts its subgoals, saves completed lemmas, and revises or refines the sketch when progress stalls.
Seed-Prover 1.5 separates these tasks among a natural-language prover, a sketch model, and an agentic Lean prover (J. Chen et al. 2025). The first proposes an informal argument. The second translates it into a Lean sketch with auxiliary lemmas and a main proof body. The third attempts to prove or disprove the unresolved lemmas. Writing the connecting proof before solving the children ensures that their eventual solutions will establish the parent goal.
Two failure signals lead to different actions. If a lemma’s proof search exhausts its budget, the system recursively decomposes that lemma. This is a decision to try a finer-grained search, not a conclusion that the lemma is intrinsically too difficult. If the lemma is disproved, the system instead revises the parent sketch. Unsuccessful search and a checked disproof must remain distinct.
The workflow initially limits search depth to four, then restarts with the lemmas already proved included in context; the authors describe the resulting effective maximum depth as eight. The new attempt can choose a different decomposition while retaining successful subproofs from the old one.
The sketch model has a different training signal from the prover. Lean checks the sketch’s formal structure, while an LLM-based rubric evaluates lemma plausibility, decomposition granularity, and whether the hardest subgoal is easier than the original problem. The rubric also penalises sketches that merely hide the original task inside a helper lemma. Formal checking establishes logical sufficiency; the learned judge estimates whether the proposed division of labour is useful.
The runtime is substantial. For the 2025 IMO problems, Seed-Prover 1.5 reports solve times of \(0.01\), \(1\), \(5\), \(8\), and \(16.5\) hours, with the sixth problem unsolved. The \(0.01\)-hour result comes from the separate Seed-Geometry solver. These are system-level solve times, not lengths of individual model responses (J. Chen et al. 2025).4
Aristotle combines lemma-based reasoning with Monte Carlo Graph Search over Lean proof states (Achim et al. 2025). Alternative proof actions are OR choices, while the subgoals created by a chosen action must all be solved, giving an AND/OR structure. It favours actions with high upper confidence bounds, then concentrates on subgoals with low lower confidence bounds—the apparent bottlenecks. It also searches negated goals to disprove false subgoals. The paper describes these choices but omits the formulas, backup rules, and implementation details needed to reproduce the search.
A file-based agent
A simpler alternative lets a general model manage the proof through a file. The basic AlphaProof Nexus agent takes a Lean file containing the target theorem and markers delimiting editable regions. It reasons, makes search-and-replace edits, and receives compiler feedback. When an episode ends with the proof incomplete, it appends a summary as a comment; the resulting file becomes the input to the next episode. Multiple subagents run independently, without sharing state (Tsoukalas et al. 2026).
The loop uses an off-the-shelf model without additional training or a separate learned evaluator of partial proofs. The policy chooses edits; Lean supplies structural feedback and checks completed proofs.
AlphaProof Nexus’s full system adds an evolutionary population of sketches, LLM-based rankings, and access to AlphaProof as a subgoal prover. It resolved nine of 353 formalised problems from the Erdős collection. A subsequent comparison on those nine successes found that the basic loop could also solve all nine. An off-the-shelf coding agent solved seven; another commercial agent and smaller-model variants solved none. Standalone AlphaProof solved none at a budget of approximately 64 TPU-hours per problem (Tsoukalas et al. 2026).
The comparison shows that a relatively simple loop can support useful mathematical search, but it does not isolate architecture from model strength or establish a general ranking of provers. It is also conditional on the nine problems the full system solved. On two of them—the two missed by the successful commercial agent—the full system reduced reported LLM expenditure by roughly a factor of two to five relative to the basic loop. On the others it was about half as cost-efficient. The reported cost comparisons exclude AlphaProof inference costs, so they are not complete compute comparisons (Tsoukalas et al. 2026).
The file and lemma-store designs share a formalisation requirement. Someone must ensure that the target statement captures the intended problem; missing library support can make an otherwise straightforward argument expensive to formalise. A correct proof of the wrong formal statement is still the wrong result. Neither a per-problem file nor a within-problem lemma cache automatically provides a curated store of new results for future problems.
Updating the policy during the run
The preceding designs can keep the policy fixed. Test-time training changes the distribution from which later attempts are drawn. Aristotle already combines these choices: at large scales, it alternates attempts on the target and its auxiliary lemmas with training on the accumulated search traces (Achim et al. 2025). This is adaptation within a formal proof search, although the report does not quantify its contribution through a component ablation.
TTRL uses majority-vote answers as pseudo-labels and runs reinforcement learning against agreement with them (Zuo et al. 2025). The apparent difficulty is circularity: a model’s own mistakes become its supervision. The paper highlights a distinction between label accuracy and reward accuracy. In its AIME 2024 analysis, majority labels are initially correct about \(37\%\) of the time, while the induced binary rewards are correct about \(92\%\) of the time.
The arithmetic is possible because most responses are wrong. When a pseudo-label is wrong, a different wrong answer still correctly receives zero reward. But a genuinely correct answer also receives zero, and responses matching the wrong pseudo-label receive an erroneous positive reward. Many correct negative labels can therefore coexist with poor positive supervision. High reward accuracy explains how noisy labels can produce mostly correct reward bits; it does not, by itself, guarantee a useful policy gradient or prevent reinforcement of an error.
The adaptation in TTRL is primarily per benchmark, with weights shared across its test questions, rather than an independent training run for each theorem. Its main evaluation is on the adapted-to questions, with additional cross-benchmark evaluations. It demonstrates adaptation to a set of problems, not yet a theorem-specific learning procedure.
Test-time curricula target individual problems more directly (Hübotter et al. 2025). They retrieve related tasks from an existing corpus, train on those tasks, and then attempt the target. The retrieved tasks already have reference answers or unit tests; the method does not solve the problem of verifying arbitrarily generated exercises. Its applicability depends on the coverage of that labelled corpus.
The targeting effect must also be separated from ordinary additional RL. On the main backbone, training on 1,000 uniformly sampled tasks recovers \(56\%\)–\(83\%\) of the targeted method’s gain over the starting model, depending on the benchmark. Across two other backbones the corresponding share ranges from \(13\%\) to more than \(100\%\): in some cases untargeted training does better (Hübotter et al. 2025). A complete comparison with fixed-policy inference must charge for curriculum construction, training, and final generation, not just the last stage.
What the evidence supports
The strongest results establish feasibility: outcome-based RL can improve single-sample performance; formal systems can retain and reuse checked subproofs; and a general model in a file-editing and verification loop can resolve some open problems (Guo et al. 2025; J. Chen et al. 2025; Tsoukalas et al. 2026). They do not yet determine the best allocation of compute across model training, sampling, decomposition, memory, and adaptation.
Compute accounting
Even the comparison between a smaller model with more inference and a larger model depends on the workload. Snell et al. (2024) make this explicit. Under their FLOP accounting, matching the total cost of a model with \(M\) times as many parameters allows the smaller model’s inference budget to be multiplied by
\[ M+3\frac{D_{\mathrm{pretrain}}}{D_{\mathrm{inference}}}(M-1), \tag{2}\]
where \(D_{\mathrm{pretrain}}\) and \(D_{\mathrm{inference}}\) are the pretraining and aggregate inference token budgets. Writing \(R=D_{\mathrm{inference}}/D_{\mathrm{pretrain}}\), values \(M\approx14\) and \(R\in\{0.16,0.79,22\}\) give multipliers of approximately \(258\), \(63\), and \(16\).
As inference load grows, the larger model’s extra training cost is amortised across more queries, and the smaller model can afford fewer additional attempts per query at equal total cost. In their experiments, larger-model pretraining is more effective on harder questions or at high inference loads. Test-time scaling is more favourable in lower-load settings. The tradeoff depends on both query volume and problem difficulty; these experiments do not establish a universal crossover at \(R=1\).
Two limitations matter here. The larger-model baseline uses greedy generation rather than its own optimised search. Conversely, estimating question difficulty uses 2,048 samples per question, while the allocated inference budgets range from 4 to 256 generations. That estimation cost—eight to 512 times the nominal budget—is excluded from the comparison. The paper discloses the issue and leaves cheaper allocation mechanisms to future work (Snell et al. 2024).
Mechanisms versus complete systems
The papers reviewed here do not provide a common, matched-compute comparison of all five designs. They use different policies, tasks, formalisation procedures, budgets, and stopping rules. Internal ablations such as the AlphaProof Nexus comparison are useful, but cannot establish an architecture’s advantage independently of those conditions.
Aristotle’s reported five-of-six IMO result, for example, establishes a capability of the complete system. Its stronger claim of favourable scaling is not accompanied by a quantitative scaling curve or results table (Achim et al. 2025). The original Seed-Prover report likewise does not isolate its architectural components, and omits model size, GPU count, and wall-clock time for its competition runs (L. Chen et al. 2025). Such results demonstrate that an approach can work; attributing the gain requires comparisons that hold the other components fixed.
Useful evaluations would report both generation coverage and selected-answer accuracy, distinguish formal proof validity from correctness of formalisation, include all tool and judging costs, and compare stateful search with independent restarts under the same budget. For long runs, success-versus-compute curves and variation across repeated runs are more informative than the solve time of one successful attempt.
What does RL change in the policy?
A related debate asks whether RL creates reasoning capabilities or concentrates probability on solutions the starting model could already produce. Some experiments find that starting models match or exceed RL-trained descendants at sufficiently large sample counts (Z. Chen et al. 2025). ProRL reports tasks on which prolonged RL reaches solutions not found by extensive sampling from its starting checkpoint (Liu et al. 2025).
The results need not be uniform across tasks or budgets. In ProRL’s AIME 2025 plot, pass@\(256\) is \(0.704\) for the starting checkpoint and \(0.665\) for the final model, despite the final model’s higher pass@\(1\). Importantly, that starting checkpoint is DeepSeek-R1-Distill-Qwen-1.5B, already a distilled reasoning model, not an unmodified pretrained base model. Other tasks, including synthetic reasoning tasks, show large gains from training. The paper reports the largest gains where the starting model’s pass@\(128\) is lowest (Liu et al. 2025).
The relevant claims are task- and budget-specific. A finite sampling experiment cannot distinguish a zero success probability from a sufficiently small one. It can establish changes in observed coverage at a stated budget. Likewise, improved pass@\(1\) need not imply improved large-\(k\) coverage.
For long-running systems, that is the useful level of analysis. Training changes the proposal distribution. Selection determines which generated solutions are returned. Persistent state changes what later attempts can condition on. Each can improve results without settling a universal question about “new capability.”
The remaining design problem
A proof checker can establish that a lemma is correct and that completed lemmas imply the target. It does not generally tell a system which lemmas are worth attempting, how much budget to give them, or when to abandon a decomposition. Reliable local verification and uncertain global search guidance therefore coexist in the same run.
The most immediate research question is how to evaluate unfinished work. A useful score need not certify a plan; it needs to predict which actions lead to progress at an acceptable cost. It should be tested through the searches it induces, rather than only through agreement with proof-quality labels. The difference between a valid decomposition and a tractable one is central to that evaluation.
A second question is how to reuse discoveries across problems, beyond the within-problem caches described above. That requires appropriate statements, preserved dependencies, retrieval, and evidence of transfer—not just saving more text. Reducing the formalisation burden would broaden the problems on which checked accumulation is practical. Test-time weight updates deserve the same treatment as other search mechanisms, with controls that separate targeted adaptation from generic training and additional sampling. The papers reviewed here leave these comparisons largely unresolved.
The asymmetry between producing and checking a proof is already an organising principle of formal search. The unresolved issue is how to exploit it when most of the run consists of incomplete attempts. Checked results provide a dependable basis for reuse; hypotheses, summaries, and value estimates still guide much of the work needed to obtain them.
To assess a system that runs for a day, ask what its verifier actually certifies, what a fresh context inherits, and how the controller chooses its next use of compute. Those details explain more about the run than its duration alone.
References
Footnotes
The reported seven false acceptances among 48 flawed proofs correspond to a \(14.6\%\) false-acceptance rate on that set. The paper prints \(41/48=87.2\%\); the quotient is \(85.4\%\). More importantly, an all-invalid set cannot establish a judge’s overall accuracy: always rejecting would score \(100\%\) there while having zero recall on valid proofs (Mahdavi et al. 2025).↩︎
R1’s reported generation cap increases from 32,768 to 65,536 tokens at training step 8.2k, alongside a jump in response length and performance. That discontinuity cannot be attributed solely to spontaneous lengthening; the paper itself discloses the cap change (Guo et al. 2025). In s1’s updated experiments, changing the teacher’s traces while keeping the 1,000 questions and training recipe fixed raises AIME 2025 accuracy from \(26.7\%\) to \(50.0\%\). For comparison, the original data-selection ablation gives a 13.3-point improvement over random selection, and budget forcing gives 6.7 points on AIME 2024; these are different comparisons, not additive causal effects. The improved s1.1 model scores \(56.7\%\) on AIME 2024 and \(50.0\%\) on AIME 2025 with zero, one, or two “Wait” insertions. Distillation quality is consequential, and extra decoding is not uniformly beneficial (Muennighoff et al. 2025).↩︎
DeepSeek-Prover-V2 reports a corrected PutnamBench score of 47/658 rather than 49/658 after excluding two misformulated statements. Of the benchmark’s 658 problems, 649 were compatible with its Lean version and actually attempted (Ren et al. 2025).↩︎
The original Seed-Prover report and Seed-Prover 1.5 describe different runs. The former reports four IMO problems completed by the submission deadline and a fifth afterwards (L. Chen et al. 2025). Four complete solutions account for 28 points; the separately circulated 30-point silver-medal figure requires partial-credit and evaluation details not given in that paper. The paper’s solve counts should not be presented as if they independently document the medal claim.↩︎