PaperlayerView exact revision on arXiv

Source-linked AI summary

h1: A Taste of the Bitter Lesson in Automated Theorem Proving

Skander Moalla, Ahmad Rammal, Niket Patel, Remi Munos, Julia Kempe

arXiv:2610.35962v1cs.LGcs.LO

TL;DR

Formal theorem proving increasingly relies on designed workflows, leaving open whether a simple loop can match them and why that matters for verifying research mathematics. This paper evaluates h1, a simple Lean harness that sustains work through feedback and reflection. At matched models and comparable cost, it matches or surpasses hand-designed workflows, while longer single attempts can outperform repetition on open problems.

  • Problem

    It is unclear whether workflow gains in formal theorem proving hold against an efficient simple loop at comparable model and compute, a question that matters as research mathematics needs mechanical verification.

    Source: §1 · p. 2

  • Method

    h1 gives a model an efficient Lean interface and sustains proof attempts through tool use, verifier feedback, and reflection without prescribing decomposition or search.

    Source: §1 · p. 2

  • Results

    At the same model and comparable cost, h1 matches or surpasses hand-designed workflows, reaches state-of-the-art benchmark results, and settles eight open problems.

    Source: §1 · p. 2, §5 · p. 10

  • Takeaways & Limitations

    The authors recommend evaluating frontier models with efficient execution feedback before prescribing workflows, while attending to interface, persistence, and context management.

    Source: §1 · p. 2, §5 · p. 10

    h1 operates on a single file and its tools cover Lean, not numerical computation, simulation, visualization, or web search.

    Source: §5 · p. 10

Abstract

from arXiv · show

While progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models, formal theorem proving has increasingly relied on human-designed workflows around these models, such as planning, decomposition, and orchestrating specialized provers. This raises a bitter-lesson question: can a simple agentic loop that scales test-time compute match these workflows? The answer matters as formal verification must scale to keep up with frontier models producing research mathematics, yet new workflows rarely settle it, as their gains are often confounded with stronger models or more compute. We study this question with h1, a simple harness that gives a model an efficient interface to Lean 4 and keeps it working through verifier feedback and self-reflection, without imposing a decomposition or search structure. h1 reaches state-of-the-art results on PutnamBench, FATE-X, and FormalConjectures100-Solved, settles eight open problems in FormalConjectures, and, at matched models, matches or outperforms specialized workflows such as Goedel-Architect and AlphaProof Nexus, surprisingly showing that a single attempt (pass@1) can often scale to solve open problems. Through ablations and matched-model comparisons with Claude Code and AxProverBase, we find that simplicity alone is not enough: an efficient Lean interface largely determines cost and solve rate. We thus recommend that future work evaluate frontier models with efficient execution feedback before prescribing workflows, at the risk of bitter lessons.

1 Introduction

The introduction asks whether a simple test-time scaling loop can match specialized theorem-proving workflows, and what such a harness must provide. It presents h1 as evidence that efficient Lean interaction and sustained attempts can make simple loops competitive.

1 Introduction

  • Formal proving has increasingly used human-designed workflows that orchestrate specialized provers or prescribe planning, decomposition, and proof refinement.The introduction contrasts this with recent interest in simple loops that provide Lean feedback and sustain work.Source: §1 · p. 2
  • The comparison matters because workflow gains are hard to assess when new systems use stronger models or more compute than their baselines.The paper frames this as an unresolved question about whether gains hold against an efficient simple loop with enough test-time compute.Source: §1 · p. 2
  • h1 sustains work through multi-turn reasoning and tool calls, formal validation, and reflection that compacts the transcript, with cost–success curves evaluated across benchmarks.The evaluation accounts for inference cost and matches models where possible.Source: §1 · p. 2
  • At matched models, h1 often matches or Pareto-dominates specialized systems, reaches state-of-the-art results on three benchmarks, and settles eight open Formal Conjectures problems.The benchmarks named are PutnamBench, FATE-X, and FormalConjectures100-Solved.Source: §1 · p. 2
  • On five Erdős problems, a longer h1 attempt can cost less than repeating h1 or APN basic, making pass@1 a budget-dependent curve.Within one run, the model can abandon an approach and try another.Source: §1 · p. 2
  • The authors conclude that simple harnesses can match or outperform complex systems, and recommend testing frontier models with efficient execution feedback before prescribing workflows.They say this lesson may plausibly extend to other structured environments.Source: §1 · p. 2

2 Methods

The methods section establishes the Lean proving task and evaluation comparisons, then describes h1’s persistent proof loop. Its design provides efficient Lean tools and verifier feedback without prescribing a proof-search structure.

2.1 Experimental setup

  • In Lean, an agent completes a proof in a source file, while compilation checks it and returns errors and open goals.Final validation can reject unfinished placeholders or added assumptions.Source: §2.1 · p. 3
  • The evaluation spans competition, qualifying-exam, and research-conjecture problems, with benchmarks selected to cover differing difficulty and saturation levels.PutnamBench mainly tests efficiency; FATE-X, FormalQualBench, and FC100-solved remain unsaturated at the study’s scale.Source: §2.1 · p. 3
  • Baselines include workflow-driven provers and simple loops, enabling comparisons of harness design as well as model progress.The workflow systems include Goedel-Architect, MerLean, and full AlphaProof Nexus; simple-loop comparisons include Humanfia, APN basic, and same-model reruns of AxProverBase and Claude Code.Source: §2.1 · p. 3
  • The paper compares inference cost with the model fixed to assess harnesses, or with the harness fixed to assess model progress.At budget B per problem, solve count includes verified proofs within budget; average cost includes failures and is capped at B.Source: §2.1 · p. 4
  • h1 runs a ReAct loop for at most T turns, editing a persistent Lean file before submission to an external validator.After rejection, a reflection LLM compacts the transcript and feedback into context for the next iteration.Source: §2.2 · p. 4
  • Rather than prescribing planning or search, h1 gives the model targeted edits, immediate compiler feedback, and optional tools for searching Mathlib and testing proof fragments.The model chooses which optional tools to use and how to develop the proof.Source: §2.2 · p. 4

3 Simple test-time scaling delivers frontier results

The section shows that frontier models in h1 reach state-of-the-art results, then tests whether simple scaling can match specialized workflows and outperform repetition on open problems. It reports benchmark results, eight newly solved open conjectures, and cases where extending one attempt is more efficient than repeating it.

3.1 A frontier model in a simple harness achieves state-of-the-art results

  • h1 with GPT-5.6 Sol reaches 90/100 on FATE-X, 78/100 on FC100-solved, 14/23 on FormalQualBench, and solves all six IMO 2026 problems.With GPT-5.5, h1 solves 670 of 672 PutnamBench problems in a single run per problem.Source: §3.1 · p. 5
  • h1 proved eight targets marked open in Formal Conjectures, including variants of Erdős 138 and 337 and three OEIS conjectures.The system also found misformalizations, including a Poincaré conjecture formalization missing a hypothesis.Source: §3.1 · p. 5, Table 1 · p. 6

3.2 The bitter lesson for specialized workflows

  • At matched models, h1 often matches or outperforms specialized workflows; on PutnamBench, DeepSeek V4 Flash reaches 598 solves against 597 for Goedel-Architect at lower estimated cost.For Putnam 2025, GPT-5.2 alone solves all twelve problems in h1, including A5, spending $81.52 on A5 against Numina’s $1,000 budget.Source: §3.2 · p. 6
  • Repetition closes most remaining gaps, but MerLean retains a one-problem advantage on FormalQualBench with Opus 4.7, even after retries.Replacing Opus 4.7 with Opus 4.8 lets h1 overtake MerLean, with 13 against 10 solves at $49.46 rather than $118.35 per solve.Source: §3.2 · pp. 6–7

3.3 Persisting can beat repetition, even on open problems

  • For Erdős 125, full APN retains an advantage over h1 because all sixteen h1 attempts end in Lean timeouts.This is a boundary case to the comparisons on the five problems all three systems solve at least once.Source: §3.3 · pp. 7–8
  • On five Erdős problems, h1 pass@1 reaches 82.5% at $138 mean spend including failures, while pass@3 needs $202 to reach at least that rate.Repetition reaches higher success rates at larger budgets, so the depth–breadth balance depends on the budget and problem.Source: §3.3 · pp. 7–8

4 What a harness must provide for efficient test-time scaling

With the same model, simple loops differ substantially in solve rate and cost; h1’s advantages come from its efficient interface, persistence, and context management. Its design supports small-step Lean interaction while leaving proof development to the model.

4 What a harness must provide for efficient test-time scaling

  • A robust interface avoids predictable failures: 42.2% of AxProverBase’s failed compilations stop at an invalid library import, which h1 avoids by importing all of Mathlib.h1 also retries transient API failures and restores its file after a Lean timeout; Humanfia spends five times more than h1 for the same 670 PutnamBench solves.Source: §4 · pp. 8–9
  • With a persistent working file, compiler feedback after every edit, and optional library search or proof-fragment testing, h1 solves 49 Putnam100 and 49 FATE-X problems without search tools, the REPL, or language server, versus 69 and 63 with all tools.Source: §4 · p. 8
  • With Gemini 3 Flash and a $20 budget, h1 solves 69 Putnam100 problems versus AxProverBase’s 18; Figure 5 shows h1 Pareto-dominating across six model settings.The figure’s comparison is at comparable or lower budget caps.Source: §4 · pp. 8–9
  • After verifier rejection, h1 continues with the working file, feedback, and a reflection summary, while Claude Code can stop without validating or give up after rejection.With Opus 4.8, FATE-X solves rise from 63 for native Claude Code to 73 with the paper’s prompt and Lean tools, while h1 reaches 83.Source: §4 · p. 9
  • With 200 turns between reflections, cached input rises from 0.2% to 86%, yet solves fall to 60 Putnam100 and 52 FATE-X; higher reasoning effort can instead improve solves at lower total cost.With Gemini 3.1 Pro, high effort solves 99 Putnam100 problems at $5.34 each, versus 89 at $20.63 with low effort.Source: §4 · pp. 9–10

5 Conclusion, limitations, and discussion

This section discusses h1’s performance and dependence on its Lean interface and harness, alongside limits in model transparency, scale, and tool coverage. It also describes the reflection prompt’s constraints on evidence, proof progress, and distinguishing work-in-progress submissions from completed proofs.

5 Conclusion, limitations, and discussion

  • h1’s simple loop with an efficient Lean interface reaches state-of-the-art results and matches or surpasses hand-designed workflows at the same model and comparable cost.A single longer attempt can outperform repetition on open problems; interface, persistence, and context management affect how efficiently compute yields progress.Source: §5 · p. 10
  • Across 707 benchmark problems, specialized workflows solved only two problems that the simple loop did not, though black-box models leave benchmark-exposure effects uncertain.The two exceptions were Erdős 125 for full APN and BurnsidePrimeDegree for MerLean with Opus 4.7; h1 with GPT-5.6 Sol proved the latter in its run.Source: §5 · p. 10
  • h1 handles single files and Lean only; larger formalizations require cross-file dependency management, codebase validation, and potentially parallel agents and richer tools.The paper recommends adding such capabilities without prescribing their use, including allowing agents to communicate freely rather than through a fixed hierarchy.Source: §5 · p. 10
  • Although h1’s interface is hand-designed, the authors argue that human effort currently helps most in interface design while compute is spent on frontier-model reasoning.They suggest that models could eventually build and deploy their own problem-specific harnesses.Source: §5 · p. 10

A Related Work

  • The related-work discussion distinguishes trained provers from harnesses around generalist models and compares selected systems using the same models, while limiting autoformalization comparisons to fixed-statement proof completion.The authors state that those results do not establish the value of the autoformalization systems in open-ended formalization.Source: A Related Work · p. 20

B Tools, Prompts, and Error Handling in h1

  • h1’s tools let the model inspect and edit a working file, search Mathlib, run Lean snippets, and access language-server goals, diagnostics, and symbols.The appendix specifies the tools, prompts, reflection safeguards, and Lean failure handling used by h1.Source: Table 3 · p. 21, B Tools, Prompts, and Error Handling… · p. 21

B.2 Prompts for proof search and reflection

  • h1 uses a multi-turn prover and a reflection model that condenses attempts and verifier feedback into context for the next iteration, without prescribing a fixed search structure.Final submissions are replayed and kernel-checked by SafeVerify, which rejects forbidden axiom dependencies and proofs that retain sorry.Source: §B.2 · pp. 21, 24, Table 4 · p. 22
  • The reflection prompt requires attributing beliefs and conclusions to the prover, while treating the proof file and verifier feedback as the only plain facts.Concrete verifier-observed tactical facts may be stated directly.Source: §B.2 · pp. 25–26
  • The prompt prohibits carrying forward cheating, defeatist reasoning, or unsupported disproofs, and directs the reflection to note neutrally why those paths did not work.It says to record concrete obstacles rather than frame a problem as open or impossible.Source: §B.2 · p. 26
  • Forced, timed-out, or tool-free submissions are treated as work-in-progress checkpoints, not as evidence that the prover gave up or finished.The prompt directs the reflection to preserve useful progress from these submissions.Source: §B.2 · p. 26
  • The reflection should preserve compiled lemmas, definitions, and Mathlib search results, along with prior context, to prevent repeated derivations and dead-end searches.It should keep this context concise and focused on maximizing prover performance.Source: §B.2 · p. 26

B.3 Lean feedback and error handling

The appendix specifies how Lean errors, proof validation, benchmark environments, and inference costs are handled. Comparisons use model-matched inference cost as a practical proxy, with explicit accounting conventions and finite budgets.

B.3 Lean feedback and error handling

  • Proof errors return to the model for revision, while process failures can trigger a restart or end execution; resumed interruptions are not new pass@k samples.A deterministic Lean failure recurring across three executions counts as unsolved; provider, cluster, and tool-service interruptions can resume from saved proof state.Source: Table 6 · p. 27, §B.3 · p. 27

C.1 Benchmark revisions and Lean environments

  • Benchmark recipes identify source revisions and Lean/Mathlib environments, with the Formal Conjectures setup pinned to revision 7862bf6a and Lean/Mathlib 4.27.0.The Formal Conjectures source date differs from the May 6 benchmark release; the comparison cutoff for state-of-the-art claims is August 27, 2026.Source: §C.1 · p. 28, Table 7 · p. 28, §C.2 · p. 29

C.2 Formal validation

  • SafeVerify checks compiled submissions against the immutable challenge, target declarations, permitted axioms, and Lean kernel; only the designated source file crosses into validation.The harness isolates compilation because SafeVerify consumes compiled .olean files, and imported modules remain part of the trusted environment.Source: §C.2 · p. 28, Table 8 · p. 29

C.3 Inference budgets and cost curves

  • Inference cost is a practical proxy for compute because providers rarely disclose FLOPs, and model-fixed cost comparisons help assess harness differences.Uncached input, cached input, cache writes, and output are priced separately; output tokens can cost up to 100× as much as cached input.Source: §C.3 · p. 29, Table 9 · p. 29
  • Budget curves count problems by first-acceptance cost, while average-cost curves use capped per-problem cost; runs stop at finite budgets or unrecoverable Lean failures.Recorded cost can exceed a nominal cap when a final model call crosses it; repeated REPL timeouts indicate a need for a better Lean interface.Source: §C.3 · pp. 29–30

C.4 PutnamBench results and published cost conventions

PutnamBench comparisons report solve percentages and costs using conventions that vary across published systems. The appendix also explains a targeted completion, estimated DeepSeek costs, uncertainty procedures, and proof screening.

C.4 PutnamBench results and published cost conventions

  • Published PutnamBench costs use nonuniform conventions, so comparisons distinguish campaign totals, per-success costs, estimates, and costs that exclude earlier attempts.The appendix cautions that Hilbert’s approximate $244 is an attributed estimate, not measured cost for its 70% headline result.Source: §C.4 · p. 30, Table 10 · p. 31
  • $5,839.36 in estimated parallel stopping cost for the targeted final two problems yields $17.86 per problem across 672 problems; full continuation cost instead gives $20.99 per problem.The estimate assumes cancellation at equal dollar cost, not equal elapsed time; the corrected formalizations also enabled other systems to reach 672 solves.Source: §C.4 · p. 31, Table 10 · p. 31

C.5 Estimated DeepSeek API costs

  • 598/672 solves at an estimated $1.08 per problem use 92.27% reconstructed cache reuse for DeepSeek V4 Flash.Cache reuse is reconstructed from unchanged prompt prefixes because local serving did not record cache-hit counters, assuming reusable prefixes remain cached.Source: §C.5 · p. 31, Table 11 · p. 32

C.6 Statistical significance and uncertainty

  • Many configurations have one run because repeating them would multiply inference cost; runs or problem resampling are used where claims require statistical significance.The appendix describes paired-problem bootstrap intervals and run-level resampling for the tool and Erdős prompt comparisons.Source: §C.6 · p. 32

C.7 Proof screening

  • Removing native_decide removes 35 accepted proofs across nine AxProverBase runs, and screened counts feed the aggregate matched-cap comparison.SafeVerify accepts the authors’ proofs and rejects sorryAx, new axioms, and evaluation via native_decide.Source: §C.7 · p. 32

D Open-Problem Proofs and Statement Corrections

The appendix records eight Formal Conjectures results and examines statement defects that can make formal targets diverge from intended mathematics. Further analyses document specialized-system exceptions, reflection effects, individual Erdős scaling curves, and prompt/model comparisons.

D.1 Statements proved

  • Eight Formal Conjectures targets were proved, with Table 12 identifying each result and its Lean proof file.Conjectures 100 and 314 were proved after statement corrections; the other six concern the named distributed targets, and each result applies to its listed formal variant.Source: Table 12 · p. 33, §D.1 · p. 33

D.2 Misformalizations and editable answers

  • Kernel checking alone does not ensure a proof expresses the intended problem: editable answers or missing hypotheses can make targets vacuous or admit unintended cases.The smooth four-dimensional Poincaré variant omitted T2Space, allowing non-Hausdorff examples; an upstream correction adds the Hausdorff assumption.Source: §D.2 · pp. 33–34, Table 13 · p. 34

E.1 Remaining advantages of specialized systems

  • Among 707 problems, BurnsidePrimeDegree and Erdős 125 were fixed-model exceptions; on Erdős 125, all 16 h1 attempts ended in unrecoverable Lean REPL timeouts.Numina solved twelve in less summed time than h1 with GPT-5.2, possibly helped by faster constituent models; Claude Code’s PutnamBench count rose from 81 to 95 with the paper’s prompt and Lean tools, while h1 reached 99.Source: §E.1 · p. 35, Figure 6 · p. 36

E.2 PutnamBench: reflection and specialized provers

  • With the same DeepSeek V4 Flash model, reflection improves h1’s PutnamBench coverage beyond Goedel-Architect’s pass@4 coverage at lower estimated cost.The same-model comparison also reports h1 substantially outperforming Goedel-Architect’s tool-integrated reasoning baseline.Source: Figure 7 · p. 36

E.3 DeepSeek V4 Flash on FC100-solved and FATE-X

  • DeepSeek V4 Flash runs on FC100-solved and FATE-X omitted self-reflection, so their curves may understate h1 with that model.The appendix says runs with self-reflection would be added in a subsequent version.Source: §E.3 · p. 36, Figure 8 · p. 37

E.4 Erdős problems: individual scaling curves

  • The Erdős scaling plots show per-problem curves across active-time cutoffs and pass@k, with cost conditional on success; all 16 Erdős 125 replicas ended in Lean REPL timeouts.Errors count as failures, and Erdős 125’s conditional cost is undefined.Source: Figure 9 · p. 37

E.5 Erdős problems: prompt and model ablations

  • The prompt comparison reports per-problem pass@1 under different prompts for both LLM roles, with all replicas included in the denominator.Figure 10 uses the same runs and $150 cap as Figure 4.Source: Figure 10 · p. 38
  • The model-scaling comparison sums per-problem pass@k estimates across six Erdős problems, while the companion per-problem bars show pass@1.Figure 11 uses a $300 per-attempt cap; Figure 12 presents the pass@1 runs from those curves.Source: Figure 11 · p. 38, Figure 12 · p. 39

E.6 Comparing success and cost with AlphaProof Nexus

The comparison evaluates h1 against AlphaProof Nexus on six Erdős problems, measuring success and cost under matched task sets and varying compute allocation. The analysis also compares model cost frontiers on PutnamBench.

E.6 Comparing success and cost with AlphaProof Nexus

  • 68.75% pass@1 across six Erdős problems is close to APN full’s 71.67%, while h1 reaches 79.73% at pass@3.Each problem receives equal weight; these are terminal outcomes, not matched-budget estimates.Source: §E.6 · p. 40, Table 15 · p. 40
  • h1’s six-problem set includes Erdős 125, where all attempts time out, unlike the five-problem conditional-cost comparison that excludes it.With no successful attempts, Erdős 125’s success-conditional cost is undefined.Source: §E.6 · p. 40, Figure 13 · p. 41
  • The unconditional cost estimate includes unsuccessful groups, since conditioning on success alone omits their spending and does not fully describe the trade-off.APN is omitted from unconditional-cost plots because its failed-group costs are unavailable.Source: §E.6 · p. 40
  • A hypothetical example shows that parallel attempts can dominate one pass@1 operating point through early-proof cancellation, but not necessarily the entire curve.The example assumes independent attempts with constant spending rates and specified solve probabilities and costs.Source: §E.6 · p. 40
  • Dollar and active-time allowances yield the same terminal costs and success rates, but different intermediate curves.Both panels average the same five problems equally and count each group’s cost through its first eligible proof.Source: §E.6 · p. 42, Figure 15 · p. 42

E.7 Model choice at different budgets

  • Leanstral 1.5 supplies the PutnamBench cost frontier through 72 solves, Gemini 3.1 Pro extends it to 99, and Gemini 3 Flash lies below it.Costs average all 100 problems, including failures; Leanstral costs are API-equivalent estimates using a measured 65% cache rate.Source: Figure 16 · p. 42

E.8 Additional comparisons with AxProverBase and analysis of failed attempts

The AxProverBase comparison finds that h1 solves additional PutnamBench problems with Gemini 3 Flash while using a different pattern of file editing, token use, and feedback handling. The appendix also reports solve-rate and failure analyses across settings.

E.8 Additional comparisons with AxProverBase and analysis of failed attempts

  • h1 overtakes AxProverBase as the budget grows across six settings, and all h1 solves pass external validation.The figure also shows AxProverBase before and after screening proofs using native_decide.Source: Figure 17 · p. 43
  • With Gemini 3 Flash, h1 solves the 18 problems solved by AxProverBase plus 51 more on the PutnamBench subset.On the 51 h1-only problems, mean proposer calls are 287 for AxProverBase and 275 for h1.Source: §E.8 · p. 43
  • Mean output tokens per problem are 5.97M for AxProverBase and 0.628M for h1, while mean input tokens are 4.24M and 23.13M, respectively.Input cache rates are 0.04% for AxProverBase and 78.8% for h1; AxProverBase regenerates candidates while h1 retains files for local edits.Source: §E.8 · p. 44
  • For AxProverBase with Gemini 3 Flash, 42.2% of failed builds first error on a bad import, compared with 0.6% for Opus 4.5; h1 records none.The figure marks reported reference values of 56% and 0.4%.Source: Figure 20 · p. 44
  • On putnam_1972_b4, AxProverBase spends $20.01 over 287 builds, while h1 solves it for $0.15 with 20 local edits, three REPL tests, and one submission.Across the 51 h1-only solves, AxProverBase performs 13,446 reflections and h1 performs 316.Source: §E.8 · p. 44

E.9 Additional comparisons with Claude Code and analysis of failed attempts

Matched Claude comparisons examine how Lean tools, validation, and continued repair relate to solve counts and failed attempts. The release-date figure distinguishes benchmark commits from public releases and cautions against inferring proprietary training exposure.

E.9 Additional comparisons with Claude Code and analysis of failed attempts

  • With the same Claude model, native Claude Code, Claude Code with Lean tools through MCP, and h1 solve 81/95/99 PutnamBench subset problems and 63/73/83 FATE-X problems, respectively.h1 additionally enforces validation and another repair round after rejection.Source: §E.9 · p. 45
  • Of 30 h1-solved problems where native Claude Code stops without an accepted proof, 28 end with artifacts rejected by SafeVerify; adding Lean tools solves 20 of them.h1 uses multiple rounds on 21 of those 30 problems.Source: §E.9 · p. 45
  • On FATE-X problem 19, Claude Code with MCP resubmits an unchanged file 170 times, whereas h1 edits after each of 17 negative outcomes and succeeds.This comparison concerns how execution continues after failures.Source: §E.9 · p. 45
  • MCP leaves API-call retries under Claude Code’s control, unlike h1’s explicit retry and verifier-failure policies.The authors note that MCP does not give the experimenter the same control over internal retries and failure handling as implementing the harness directly.Source: §E.9 · p. 45

E.10 Model and benchmark release dates

  • Benchmark dates marked with an asterisk are first benchmark-containing commits, not verified public-release dates, and do not establish proprietary training-data contents.Dates distinguish possible exposure to statements, formalizations, and published solutions.Source: Figure 21 · p. 45

F Tool, Prompt, and Reflection Ablations

The ablations compare tool configurations, prompt variants, reflection inputs and intervals, and reasoning effort. They find that tool capabilities and prompt detail improve coverage, while reflection timing and context involve distinct solve-rate or cost trade-offs.

F Tool, Prompt, and Reflection Ablations

  • The detailed prompt improves solve rates on the PutnamBench subset and FATE-X, with crashes included in the denominator.The settings are Gemini 3 Flash at $20 per problem and Gemini 3.1 Pro at $50.Source: Figure 23 · p. 46
  • Full-transcript and distilled-final-attempt reflection yield 69 versus 67 PutnamBench solves and 63 versus 64 FATE-X solves in these runs.Each arm contains 100 problems and one run; per-problem caps are $20 and $50, including prover and reflection calls.Source: Figure 24 · p. 47
  • Removing the reflection transcript cuts reflection input costs by 95% on PutnamBench and 90% on FATE-X, but raises prover-call costs by 9.6% and 7.3%, respectively.The increase occurs on 64/100 and 74/100 problems; total-cost changes remain small, with intervals spanning zero.Source: F Tool, Prompt, and Reflection Ablations · p. 47, Table 16 · p. 47
  • Adding tools to the working-file baseline retains all 49 PutnamBench solves and adds 20, while on FATE-X it retains 48 of 49 and adds 15.The other tool configurations substantially overlap, and removing any single tool has little effect on coverage.Source: Figure 22 · p. 46, Figure 25 · p. 48
  • Reflection every proof-search turn produces fewer solves over most observed budgets; intervals of 10 and 50 turns give similar curves.The tested intervals range from 1 to 200 turns on the PutnamBench subset and FATE-X.Source: Figure 27 · p. 49
  • More reasoning per turn can make test-time scaling more efficient in the Gemini 3.1 Pro PutnamBench comparison.The figure compares low, medium, and high reasoning effort using solves against mean cost, including failed attempts.Source: Figure 28 · p. 50
  • The token and cost analysis averages input, cached input, and output tokens, reports cache fractions, and includes both prover and reflection calls.It compares reflection intervals on PutnamBench with Gemini 3 Flash and FATE-X with Gemini 3.1 Pro.Source: Figure 29 · p. 50, F Tool, Prompt, and Reflection Ablations · p. 50

G Solve-Time and Proof-Size Statistics

The figures summarize solve time and accepted-proof length across four state-of-the-art runs, with cumulative distributions showing acceptance rates and medians among accepted proofs.

G Solve-Time and Proof-Size Statistics

  • The selected runs’ largest reported values—1,123 iterations, 95 active hours, and a 7,124-line proof—come from other runs.The maxima were recorded on PutnamBench, FATE-X, and the Borsuk–Ulam theorem, respectively.Source: G Solve-Time and Proof-Size Statistics · p. 51
  • 852 proofs were accepted in 895 attempts across PutnamBench, FATE-X, FormalQualBench, and FC100-solved runs.The selected runs include 670/672 PutnamBench problems with GPT-5.5, and 90/100, 14/23, and 78/100 on the other benchmarks with GPT-5.6 Sol.Source: Figure 30 · p. 51, Figure 32 · p. 52
  • Figure 30’s left panel measures active hours to first acceptance, while its right panel measures accepted Lean-file length.Densities are estimated in log10 space and normalized so their area equals the benchmark’s acceptance percentage.Source: Figure 30 · p. 51
  • Figure 31 plots cumulative distributions with counts divided by all attempted problems; diamonds mark medians among accepted proofs.Each curve therefore ends at that run’s acceptance percentage.Source: Figure 31 · p. 52

H Reproducibility

The paper describes its reproduction materials across the main text and appendices, covering the harness, validation, budgets, aggregation, and ablation settings.

H Reproducibility

  • Section 2.2 and Appendix B describe the harness, including its tools, prompts, and reflection protocol.The paper says it includes detail to support reproduction of the harness and figure-plotting procedures.Source: H Reproducibility · p. 53
  • Appendix C documents formal validation, inference budgets, pricing, and cost-capped curve construction.Source: H Reproducibility · p. 53
  • Appendix E.6 details aggregation and uncertainty estimates, while Appendix F specifies the ablation settings.Source: H Reproducibility · p. 53

Related papers

Loading 2610.35962v1…