Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing

# Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
Source: [https://arxiv.org/html/2608.28639](https://arxiv.org/html/2608.28639)
###### Abstract

Formal theorem proving with large language models remains challenging due to the difficulty of navigating large proof search spaces efficiently\. Existing tree search approaches either feed verbose compiler error messages directly into the generation context, increasing context usage during search, or employ non\-standard evaluation protocols that prevent direct comparison with established baselines\. We propose a three\-role Monte Carlo Tree Search \(MCTS\) framework that treats the Lean 4 compiler purely as a reward oracle using compiler output as a scalar signal for UCB\-guided tree updates without feeding error content into the generation context\. Our framework decomposes proof search into three roles: a generator for proof attempts, a decomposer for subgoal decomposition, and a critic for subgoal quality evaluation\. We evaluate across 4 benchmarks spanning competition mathematics and physics \(MiniF2F, PutnamBench, LeanPhysBench, PhysLeandata\) with three prover models at standard proof attempt budgets \(PAB@16 to PAB@256\)\. Our method achieves 87\.1% on MiniF2F with Goedel\-Prover\-V2\-8B at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 surpassing base sampling 18/659 at same proof attempt budget\. Through an exhaustive axiom\-level audit of every compiled proof, we further identify reward hacking in search\-based theorem proving: DeepSeek\-Prover\-V2\-7B produces proofs on PutnamBench that pass compilation and the standard sorry\-token scan while depending on sorryAx\. The audit removes 4 and 8 such proofs from whole\-proof sampling at PAB@32 and PAB@128, and 11 and 19 from MCTS\. We do not attribute these counts to the search procedure; we report them to establish that kernel\-level auditing is necessary for compiler\-verified evaluation\.

## Introduction

Formal theorem proving with large language models has emerged as a challenging frontier in AI reasoning, requiring models to navigate exponentially large proof search spaces while satisfying the strict correctness requirements of interactive theorem provers such as Lean 4\(de Moura and Ullrich[2021](https://arxiv.org/html/2608.28639#bib.bib13)\)and Isabelle\(Nipkowet al\.[2002](https://arxiv.org/html/2608.28639#bib.bib14)\)\. Recent advances in specialized prover models\(Linet al\.[2025c](https://arxiv.org/html/2608.28639#bib.bib15); Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17); Wanget al\.[2025](https://arxiv.org/html/2608.28639#bib.bib16)\)have demonstrated promising results on established benchmarks, yet the fundamental challenge of efficiently exploring proof search spaces remains open\.

We propose a three\-role Monte Carlo Tree Search \(MCTS\) framework built around a distinct architectural principle: the Lean 4 compiler is used exclusively as areward oracle, rather than as a source of textual feedback for subsequent generations\. Unlike compiler\-guided approaches that append error messages or proof\-state diagnostics to the model context, our method converts compilation outcomes into scalar rewards that are propagated through the search tree and used only for UCB\-guided node selection\. This separation between verification and generation prevents compiler feedback from accumulating with search depth, while still allowing formal verification signals to influence future exploration through value backpropagation\. Consequently, the framework performs iterative, verifier\-guided search over natural\-language proof plans without requiring compiler\-error\-conditioned generation\.

Our framework decomposes proof search into three distinct roles: ageneratorthat produces complete proof attempts, adecomposerthat breaks problems into subgoals with temperature\-decayed sampling to balance exploration and exploitation, and acriticthat evaluates subgoal quality to provide a richer reward signal than binary compiler output alone\. At each MCTS iteration, the UCB policy traverses the current tree from the root to select a leaf node based on backpropagated compiler and critic rewards\.

We restrict our primary comparison to whole\-proof sampling on the same frozen checkpoint, rather than to methods such as BFS\-Prover\(Xinet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib44)\), HunyuanProver\(Liet al\.[2025a](https://arxiv.org/html/2608.28639#bib.bib45)\), which retrain or fine\-tune the underlying prover model\. Because these methods change the checkpoint itself via retrained value/policy networks, additional RL, or adversarially generated training data any performance delta conflates search\-procedure gains with model gains, and cannot isolate the contribution of the search algorithm\. Whole\-proof sampling provides the cleanest primary baseline for isolating the effect of inference\-time search while holding the prover checkpoint fixed\. We additionally compare with inference\-time structured\-search baselines that use the same frozen checkpoints, prompts, and evaluation environment\. Throughout the paper, we use the terms proof attempt budget and budget interchangeably, and denote it byP​A​B​@PAB@\.

We evaluate across four benchmarks spanning competition mathematics and theoretical physics MiniF2F\(Zhenget al\.[2022](https://arxiv.org/html/2608.28639#bib.bib23)\), PutnamBench\(Tsoukalaset al\.[2024](https://arxiv.org/html/2608.28639#bib.bib24)\), LeanPhysBench\(Liet al\.[2025b](https://arxiv.org/html/2608.28639#bib.bib25)\), and PhysLeandata\(Zhanget al\.[2026](https://arxiv.org/html/2608.28639#bib.bib26)\)using three specialized prover models \(Goedel\-Prover\-V2\-8B\(Linet al\.[2025c](https://arxiv.org/html/2608.28639#bib.bib15)\), DeepSeek\-Prover\-V2\-7B\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\), Kimina\-Prover\-Preview\-Distill\-7B\(Wanget al\.[2025](https://arxiv.org/html/2608.28639#bib.bib16)\)\) at standard proof attempt budgets \(PAB@16 to PAB@256\)\. On PutnamBench, our method solves 26/659 problems with Goedel\-Prover\-V2\-8B at PAB@32 surpassing base sampling’s 18/659 at same proof attempt budget\. On MiniF2F, our method achieves 87\.1% with Goedel\-Prover\-V2\-8B at PAB@256 and continues to improve consistently as the proof attempt budget increases\.

Beyond strong empirical results, we identify and characterize a reward\-hacking phenomenon\. DeepSeek\-Prover\-V2\-7B, which was previously reported to exploit a Lean 4\.9\.0 interface vulnerability\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\), produces exploit\-dependent successful proofs under both whole\-proof sampling and MCTS on PutnamBench\. At PAB@32, the audit removes 4 successful proofs from whole\-proof sampling and 11 from MCTS; at PAB@128, it removes 8 and 19, respectively\. This finding highlights a fundamental evaluation risk, making kernel\-level proof auditing essential for search\-based theorem\-proving evaluation\. We further conduct a systematic multi\-agent analysis showing that, for the evaluated models, selectively using a heterogeneous critic can improve proof search, whereas heterogeneous decomposition consistently degrades performance\.

## Related work

### Formal Theorem Proving with Large Language Models

Early approaches to neural theorem proving focused on training specialized models to generate complete proof attempts in a single forward pass\(Firstet al\.[2023](https://arxiv.org/html/2608.28639#bib.bib42)\)\. GPT\-f\(Polu and Sutskever[2020](https://arxiv.org/html/2608.28639#bib.bib27)\)demonstrated that language models pretrained on mathematical text could generate useful proof steps when fine\-tuned on proof corpora, establishing the foundation for subsequent work\. ReProver\(Yanget al\.[2023](https://arxiv.org/html/2608.28639#bib.bib28)\)introduced retrieval\-augmented generation for tactic prediction, improving performance by conditioning proof generation on relevant premises retrieved from Mathlib\.

### Tree Search for Theorem Proving

Tree search methods have a long history in formal reasoning\(Dong and Ma[2025](https://arxiv.org/html/2608.28639#bib.bib43); Xinet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib44); Liet al\.[2025a](https://arxiv.org/html/2608.28639#bib.bib45)\)\. HyperTree Proof Search\(Lampleet al\.[2022](https://arxiv.org/html/2608.28639#bib.bib21)\)applies Monte Carlo Tree Search \(MCTS\) to Lean proof search using a learned value function jointly trained with the proof model to guide node expansion\. COPRA\(Thakuret al\.[2024](https://arxiv.org/html/2608.28639#bib.bib19)\)performs context\-sensitive proof search by maintaining proof state across attempts and incorporating compiler feedback into subsequent generations\. Draft\-Sketch\-Prove\(Jianget al\.[2023](https://arxiv.org/html/2608.28639#bib.bib22)\)decomposes proofs into high\-level sketches that are subsequently completed by a tactic model, anticipating the use of intermediate proof decomposition\. ReProver\(Yanget al\.[2023](https://arxiv.org/html/2608.28639#bib.bib28)\)improves tactic prediction through retrieval\-augmented generation, while Prover Agent\(Babaet al\.[2026](https://arxiv.org/html/2608.28639#bib.bib18)\)performs iterative compiler\-guided search within a tree\-based framework\.

### Monte Carlo Tree Search in Language Model Reasoning

MCTS has been applied broadly to improve LLM reasoning beyond theorem proving\.Yaoet al\.\([2023](https://arxiv.org/html/2608.28639#bib.bib29)\)introduced Tree of Thoughts, using LLM\-guided search over reasoning steps with value estimation for intermediate states\.Haoet al\.\([2023](https://arxiv.org/html/2608.28639#bib.bib30)\)proposed Reasoning via Planning, applying MCTS with LLM\-based world models for multi\-step reasoning tasks\.Fenget al\.\([2024](https://arxiv.org/html/2608.28639#bib.bib31)\)extended AlphaZero\-style self\-play to mathematical reasoning, training value and policy networks jointly\.

### Whole\-Proof Generation

A complementary research direction focuses on whole\-proof generation\(Firstet al\.[2023](https://arxiv.org/html/2608.28639#bib.bib42)\), where the model generates a complete Lean proof script in a single pass, typically accompanied by an extended reasoning trajectory\. Recent advances in this paradigm have been driven by two major approaches\. The first employs expert\-iteration frameworks, which iteratively incorporate successfully verified proofs into the training corpus to progressively improve the prover\(Poluet al\.[2022](https://arxiv.org/html/2608.28639#bib.bib47); Wuet al\.[2021](https://arxiv.org/html/2608.28639#bib.bib48),[2025](https://arxiv.org/html/2608.28639#bib.bib49); Linet al\.[2025a](https://arxiv.org/html/2608.28639#bib.bib50); Dong and Ma[2025](https://arxiv.org/html/2608.28639#bib.bib43); Linet al\.[2025b](https://arxiv.org/html/2608.28639#bib.bib51),[c](https://arxiv.org/html/2608.28639#bib.bib15)\)\. The second leverages reinforcement learning guided by proof\-assistant verification signals, enabling models to refine proof generation through verifier\-based feedback\(Kaliszyket al\.[2018](https://arxiv.org/html/2608.28639#bib.bib52); Xinet al\.[2024](https://arxiv.org/html/2608.28639#bib.bib53); Zhanget al\.[2025](https://arxiv.org/html/2608.28639#bib.bib54); Wanget al\.[2025](https://arxiv.org/html/2608.28639#bib.bib16); Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17); Gloeckleet al\.[2024](https://arxiv.org/html/2608.28639#bib.bib55); Jiet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib56); Linet al\.[2025c](https://arxiv.org/html/2608.28639#bib.bib15)\)\.

### Reward Hacking in Reinforcement Learning

Reward hacking where agents exploit unintended patterns in reward signals rather than solving the intended task is a well\-documented failure mode in reinforcement learning\(Wanget al\.[2026](https://arxiv.org/html/2608.28639#bib.bib34)\)\. In the LLM context, reward hacking has been observed in RLHF settings where models learn to exploit reward model weaknesses\(Gaoet al\.[2022](https://arxiv.org/html/2608.28639#bib.bib35)\)\. In formal theorem proving specifically,Renet al\.\([2025](https://arxiv.org/html/2608.28639#bib.bib17)\)reported that DeepSeek\-Prover\-V2\-7B exploited a Lean 4\.9\.0 compiler vulnerability where theapply?tactic failed to emitsorrydeclarations under certain conditions producing proofs that passed compilation without being mathematically valid\.

### Lean 4 Proof Evaluation Infrastructure

Automated evaluation of Lean 4 proofs requires interactive theorem prover infrastructure that can compile tactic\-level proof attempts and return verification results programmatically\. Several tools have been developed for this purpose, each with different design tradeoffs\.

LeanDojo\(Yanget al\.[2023](https://arxiv.org/html/2608.28639#bib.bib28)\)is an open\-source framework that provides a programmatic interface to Lean 4 through a REPL\-based interaction model, enabling extraction of proof states, tactic execution, and premise retrieval from Mathlib\. LeanDojo has become the standard evaluation infrastructure for many theorem proving benchmarks including MiniF2F and PutnamBench, and its premise extraction capabilities underpin retrieval\-augmented approaches such as ReProver\(Yanget al\.[2023](https://arxiv.org/html/2608.28639#bib.bib28)\)\.

LeanInteract\(Poirouxet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib39)\)extends the REPL\-based approach with improved session management and support for parallel proof evaluation, reducing the overhead of maintaining multiple concurrent Lean processes\. PyPantograph\(Anivaet al\.[2024](https://arxiv.org/html/2608.28639#bib.bib40)\)takes a different approach, providing a Python\-native interface to the Lean 4 kernel through direct FFI bindings rather than a REPL subprocess\.

Kimina Lean Server\(Santoset al\.[2025](https://arxiv.org/html/2608.28639#bib.bib41)\)is purpose\-built for large\-scale parallel proof evaluation in the context of reinforcement learning and tree search methods\. Unlike REPL\-based tools that maintain sequential interaction with a single Lean process, Kimina Lean Server manages a pool of persistent Lean REPL instances that handle concurrent proof compilation requests enabling high\-throughput evaluation at the sampling budgets required by tree search methods\. The server exposes an HTTP interface that accepts complete Lean 4 proof strings and returns compilation results including success status, error messages, andsorryusage detection\. Our method uses Kimina Lean Server as the compiler reward oracle throughout all experiments\.

## Comparison with Existing Inference\-Time Search Methods

To clarify the algorithmic distinctions between our framework and prior inference\-time search methods for formal theorem proving, Table[1](https://arxiv.org/html/2608.28639#Sx3.T1)summarizes the major design choices\. Unlike methods that condition future generation on compiler feedback or proof\-state diagnostics, our approach treats the Lean verifier exclusively as a*reward oracle*: only the scalar reward is propagated through MCTS, while compiler messages are never inserted into the LLM context\. Furthermore, our search operates over natural\-language proof plans rather than formal proof states, allowing the search policy to allocate compute through UCB\-guided exploration while remaining independent of compiler\-specific feedback\.

Table 1:Architectural comparison between our framework and closely related inference\-time search methods\. “Compiler usage” refers to how Lean verification is incorporated into the search process\.MethodSearchSearchGenerator ReceivesLLMSearchRewardRepresentationStrategyCompiler FeedbackCriticAllocationBackprop\.COPRAFormal proof stateSequential refinement✓ Compiler text–Fixed–Prover AgentProof attemptsTree refinement✓ Compiler text–Heuristic expansionMethod\-specificBFS\+CGNatural\-language plansBreadth\-first×\\times\(scalar evaluation only\)✓Breadth\-first–One\-shot decompositionNatural\-language plansSingle expansion×\\times\(scalar evaluation only\)✓Flat expansion–Reward\-Oracle MCTS \(Ours\)Natural\-language proof plansUCB\-guided MCTS×\\timesScalar reward only✓Adaptive✓

## Method

Our framework decomposes proof search into three specialized roles: agenerator, adecomposer, and acriticcoordinated by a Monte Carlo Tree Search procedure\. Each nodend,kPn^\{P\}\_\{d,k\}in the search tree represents a subgoal state at depthdd, child indexkk, with parent nodePP\(whereP=rP\{=\}rdenotes the root\)\. The tree is initialized with a single root noden0,0rn^\{r\}\_\{0,0\}corresponding to the original theoremTT\. We describe the four phases of each MCTS iteration below, with the overall procedure illustrated in Figure[1](https://arxiv.org/html/2608.28639#Sx4.F1)\. Throughout this paper, “states” in our method refer to natural\-language proof\-plan search states rather than formal Lean 4 proof states\.

![Refer to caption](https://arxiv.org/html/2608.28639v1/x1.png)Figure 1:Overview of the proposed search framework\. Each nodend,NPn^\{P\}\_\{d,N\}represents thekk\-th child at depthdd, with parentPP:PP=rrdenotes the root\.### Selection

Beginning from the root noden0,0rn^\{r\}\_\{0,0\}, the selection phase traverses the tree by repeatedly choosing the child node that maximizes the UCB criterion:

UCB​\(nd,kP\)=Q​\(nd,kP\)\+c​ln⁡N​\(parent​\(nd,kP\)\)N​\(nd,kP\)\\text\{UCB\}\(n^\{P\}\_\{d,k\}\)\\;=\\;Q\(n^\{P\}\_\{d,k\}\)\\;\+\\;c\\sqrt\{\\frac\{\\ln N\\\!\\left\(\\text\{parent\}\(n^\{P\}\_\{d,k\}\)\\right\)\}\{N\(n^\{P\}\_\{d,k\}\)\}\}\(1\)
whereQ​\(n\)Q\(n\)is the empirical mean rollout reward of nodenn,N​\(n\)N\(n\)is its visit count, andc=2c=\\sqrt\{2\}is the exploration constant\. For an unvisited node, the exploration term is treated as\+∞\+\\infty, ensuring that every newly generated child is evaluated before previously visited children are reselected\. Traversal continues until a leaf node is reached that is either terminal or has not yet been fully expanded\. If the selected node is non\-terminal and has not yet been expanded, it is expanded intoKKchild nodes\. Previously expanded internal nodes remain eligible for future traversal, and their children are repeatedly selected according to the UCB policy as the search proceeds\. Thus, the tree is incrementally refined over successive iterations as visit counts and value estimates are updated through backpropagation\.

### Expansion

The selected nodennat depthddis expanded by generatingK=4K\{=\}4child subgoals \(gkg\_\{k\}\) using the decomposer role\. The decomposer is prompted with the original theorem and the trajectory from the root to the current node, namely, the sequence of subgoals accumulated along that path\. It proposes the next intermediate proof step as a natural language subgoal, producingKKdiverse candidates that become child nodesnd\+1,1n,…,nd\+1,Knn^\{n\}\_\{d\+1,1\},\\ldots,n^\{n\}\_\{d\+1,K\}in the tree\.

A key design choice in expansion istemperature decay: the decomposer sampling temperatureτd\\tau\_\{d\}is annealed according to both the current depthddand the iteration indexiias:

τd=τ0⋅e−0\.12​d⋅e−0\.03​ln⁡\(1\+i\)\\tau\_\{d\}\\;=\\;\\tau\_\{0\}\\cdot e^\{\-0\.12\\,d\}\\cdot e^\{\-0\.03\\ln\(1\+i\)\}\(2\)
starting fromτ0=0\.7\\tau\_\{0\}\{=\}0\.7\. At shallow depths and early iterations, the higher temperature encourages diverse subgoal proposals, enabling broad exploration of distinct proof strategies\. At greater depths and later iterations, the lower temperature concentrates sampling on more focused, committed proof directions\. This schedule directly governs the exploration–exploitation balance of the search\. Our ablation analysis, provided in the supplementary appendix submitted with the paper, shows that removing temperature decay consistently degrades performance across the evaluated models, indicating that it is a critical architectural component of our framework\.

### Evaluation

Each newly expanded child nodend\+1,knn^\{n\}\_\{d\+1,k\}is evaluated using two complementary reward signals that together form the rollout rewardrt=rc\+rsr\_\{t\}=r\_\{c\}\+r\_\{s\}\.

#### Critic rewardrc∈\[0,1\]r\_\{c\}\\in\[0,1\]\.

The critic role assesses the quality of the proposed subgoalgkg\_\{k\}by sampling the critic LLM five times at a fixed low temperature ofτ=0\.3\\tau\{=\}0\.3and averaging the scores\. The low temperature ensures stable, consistent evaluation rather than diverse sampling\. The critic provides a soft quality signal that compensates for the binary nature of compiler feedback a subgoal that does not immediately yield a compiling proof may still receive high critic reward if it represents a promising intermediate step toward the final proof\. The critic outputs a scorer^c∈\[0,100\]\\hat\{r\}\_\{c\}\\in\[0,100\], which we normalize asrc=r^c/100∈\[0,1\]r\_\{c\}=\\hat\{r\}\_\{c\}/100\\in\[0,1\]\.

#### Server rewardrs∈\[0,1\]r\_\{s\}\\in\[0,1\]\.

The generator role producesSScomplete Lean 4 proof attempts for each child node, conditioned on the full trajectory from root to that node at a fixed temperature ofτ=0\.7\\tau\{=\}0\.7\. Each attempt is submitted to the Kimina Lean server\(Santoset al\.[2025](https://arxiv.org/html/2608.28639#bib.bib41)\), which compiles the proof and checks for the absence ofsorrydeclarations\. Letsks\_\{k\}denote the number of attempts that compile successfully\. We define the normalized server reward asrs=sk/Sr\_\{s\}=s\_\{k\}/S,rs∈\{0,1/S,2/S​…,1\}r\_\{s\}\\in\\\{0,1/S,2/S\\ldots,1\\\}\. Crucially, we use compiler output solely as a scalar count signal no error message content is fed back into the generation context\.

### Backpropagation

After rollout evaluation, the obtained rollout rewardrtr\_\{t\}is propagated from the expanded node back to the root along the selected search path\. For every node on this path, the visit count and cumulative reward are updated as

N​\(n\)←N​\(n\)\+1,W​\(n\)←W​\(n\)\+rt,N\(n\)\\leftarrow N\(n\)\+1,\\qquad W\(n\)\\leftarrow W\(n\)\+r\_\{t\},and the node value used by UCB is computed as

Q​\(n\)=W​\(n\)N​\(n\)\.Q\(n\)=\\frac\{W\(n\)\}\{N\(n\)\}\.These updates follow the standard MCTS backpropagation procedure\. These updated statistics are subsequently used by the UCB selection policy during future iterations to balance exploration and exploitation\.

After backpropagation, the next iteration begins with a fresh selection phase from the root\. The updated visit counts and value estimates allow the UCB policy to allocate more search effort to promising subtrees while continuing to explore less\-visited alternatives\.

### Proof attempt Budget

At each ofNNMCTS iterations, one leaf node is selected according to the UCB policy and expanded intoKKchild nodes\. Each child is evaluated usingSScomplete proof attempts, resulting inK×SK\\times Sgenerator rollouts per iteration\. Therefore, the total proof\-attempt sampling budget is exactlyN×K×SN\\times K\\times Sper problem\. We scale the proof attempt budget by varyingSSwhile keepingNNandKKfixed:

PAB@​B=N×K×S=4×4×S\\text\{PAB@\}B\\;=\\;N\\times K\\times S\\;=\\;4\\times 4\\times S\(3\)
givingS=2S\{=\}2for PAB@32,S=4S\{=\}4for PAB@64,S=8S\{=\}8for PAB@128, andS=16S\{=\}16for PAB@256\. Throughout this paper, PAB@B denotes proof\-attempt budget\.

Table 2:Results on the miniF2F test set for different methods\. All results are averaged over 5 random seeds\.ModelMethodSizeGeneratorDecomposerCriticSuccess \(%\)completionscompletionscompletionsKiminaBFS\+CG7B4×2×44\\times 2\\times 44×44\\times 44×44\\times 462\.5±0\.662\.5\\pm 0\.6One\-shot decomposition16×2×116\\times 2\\times 116×116\\times 116×116\\times 161\.3±0\.661\.3\\pm 0\.6Agent \(ours\)4×2×44\\times 2\\times 44×44\\times 44×44\\times 464\.3±0\.8\\mathbf\{64\.3\\pm 0\.8\}DeepSeekBFS\+CG7B4×2×44\\times 2\\times 44×44\\times 44×44\\times 475\.4±0\.675\.4\\pm 0\.6One\-shot decomposition16×2×116\\times 2\\times 116×116\\times 116×116\\times 174\.5±0\.374\.5\\pm 0\.3Agent \(ours\)4×2×44\\times 2\\times 44×44\\times 44×44\\times 477\.1±0\.3\\mathbf\{77\.1\\pm 0\.3\}GoedelBFS\+CG8B4×2×44\\times 2\\times 44×44\\times 44×44\\times 482\.7±0\.482\.7\\pm 0\.4One\-shot decomposition16×2×116\\times 2\\times 116×116\\times 116×116\\times 181\.7±0\.481\.7\\pm 0\.4Agent \(ours\)4×2×44\\times 2\\times 44×44\\times 44×44\\times 484\.2±0\.5\\mathbf\{84\.2\\pm 0\.5\}
- •BFS indicates breadth first search, CG indicates critic guided search

Table 3:Results on miniF2F test set for different proof attempt budgets and methods\. All results are averaged over 5 random seeds\. Prover Agent is reproduced under our evaluation setting at a proof attempt budget of 260, since only at this budget does its full iterative\-refinement pipeline execute\.ModelMethodSizeBudgetSuccess \(%\)KiminaWhole\-proof7B3262\.8±0\.862\.8\\pm 0\.86465\.1±0\.365\.1\\pm 0\.3Agent \(ours\)3264\.3±0\.864\.3\\pm 0\.86466\.9±0\.2\\mathbf\{66\.9\\pm 0\.2\}DeepSeekWhole\-proof7B3275\.2±0\.575\.2\\pm 0\.56476\.3±0\.776\.3\\pm 0\.712877\.5±0\.377\.5\\pm 0\.325678\.2±0\.178\.2\\pm 0\.1Prover Agent26081\.7±0\.381\.7\\pm 0\.3Agent \(ours\)3277\.1±0\.377\.1\\pm 0\.36479\.3±0\.479\.3\\pm 0\.412881\.4±0\.281\.4\\pm 0\.225682\.6±0\.1\\mathbf\{82\.6\\pm 0\.1\}GoedelWhole\-proof8B3282\.4±0\.682\.4\\pm 0\.66483\.3±0\.483\.3\\pm 0\.412883\.9±0\.283\.9\\pm 0\.225684\.7±0\.184\.7\\pm 0\.1Prover Agent26086\.2±0\.186\.2\\pm 0\.1Agent \(ours\)3284\.2±0\.584\.2\\pm 0\.56485\.6±0\.485\.6\\pm 0\.412886\.3±0\.286\.3\\pm 0\.225687\.1±0\.2\\mathbf\{87\.1\\pm 0\.2\}Table 4:Results on miniF2F test set for reward ablations\. All results are averaged over 5 random seeds\.ModelMethodSizePABSuccess \(%\)DeepSeekAgent \(critic only\)7B3273\.7±0\.773\.7\\pm 0\.76474\.2±0\.374\.2\\pm 0\.3Agent \(critic\+reward\)3277\.1±0\.377\.1\\pm 0\.36479\.3±0\.479\.3\\pm 0\.412881\.4±0\.281\.4\\pm 0\.225682\.6±0\.182\.6\\pm 0\.1GoedelAgent \(critic only\)8B3281\.6±0\.681\.6\\pm 0\.66482\.5±0\.582\.5\\pm 0\.5Agent \(critic\+reward\)3284\.2±0\.584\.2\\pm 0\.56485\.6±0\.485\.6\\pm 0\.412886\.3±0\.286\.3\\pm 0\.225687\.1±0\.2\\mathbf\{87\.1\\pm 0\.2\}Table 5:Results on PutnamBench for different methods and proof attempt budgets\. Following prior PutnamBench evaluations, results are reported as a single benchmark run over all 659 problemsModelMethodSizePAB\#SolvedDeepSeekWhole\-proof7B329/65932∗𝟏𝟑/𝟔𝟓𝟗\\mathbf\{13/659\}12810/659128∗𝟏𝟖/𝟔𝟓𝟗\\mathbf\{18/659\}Agent \(ours\)3216/65932∗𝟐𝟕/𝟔𝟓𝟗\\mathbf\{27/659\}12825/659128∗𝟒𝟒/𝟔𝟓𝟗\\mathbf\{44/659\}GoedelWhole\-proof8B3218/65912822/659Agent \(ours\)3226/65912836/65936/659
∗Potential exploit\.

Table 6:Results on PhysLeandata test set\. Results are averaged across 5 random seeds\.ModelMethodSizePABSuccess \(%\)KiminaWhole\-proof7B1625\.2±0\.625\.2\\pm 0\.6Agent \(critic\+reward\)1627\.5±0\.6\\mathbf\{27\.5\\pm 0\.6\}DeepSeekWhole\-proof7B1633\.8±0\.533\.8\\pm 0\.5Agent \(critic\+reward\)1636\.2±0\.6\\mathbf\{36\.2\\pm 0\.6\}GoedelWhole\-proof8B1631\.9±0\.731\.9\\pm 0\.7Agent \(critic\+reward\)1633\.8±0\.4\\mathbf\{33\.8\\pm 0\.4\}Table 7:Results on LeanPhysBench \(proof attempt budget \(PAB@B\) = 16\)\. Results are averaged across 5 random seeds\. The PhysLib library is directly passed as context\. Critic\+server rewards used for all our method configurations\.ModelMethodSuccess \(%\)KiminaWhole\-proof9\.3±0\.39\.3\\pm 0\.3Whole\-proof \(w/ PhysLib\)13\.5±0\.713\.5\\pm 0\.7Agent \(ours, no PhysLib\)11\.5±0\.611\.5\\pm 0\.6Agent \(ours, w/ PhysLib\)15\.0±0\.7\\mathbf\{15\.0\\pm 0\.7\}DeepSeekWhole\-proof11\.5±0\.211\.5\\pm 0\.2Whole\-proof \(w/ PhysLib\)14\.5±0\.214\.5\\pm 0\.2Agent \(ours, no PhysLib\)13\.0±0\.413\.0\\pm 0\.4Agent \(ours, w/ PhysLib\)16\.5±0\.6\\mathbf\{16\.5\\pm 0\.6\}GoedelWhole\-proof10\.0±0\.210\.0\\pm 0\.2Whole\-proof \(w/ PhysLib\)15\.0±0\.215\.0\\pm 0\.2Agent \(ours, no PhysLib\)12\.0±0\.412\.0\\pm 0\.4Agent \(ours, w/ PhysLib\)16\.5±0\.3\\mathbf\{16\.5\\pm 0\.3\}

## Results

We evaluate our framework across four benchmarks MiniF2F\(Zhenget al\.[2022](https://arxiv.org/html/2608.28639#bib.bib23)\), PutnamBench\(Tsoukalaset al\.[2024](https://arxiv.org/html/2608.28639#bib.bib24)\), PhysLeandata\(Zhanget al\.[2026](https://arxiv.org/html/2608.28639#bib.bib26)\), and LeanPhysBench\(Liet al\.[2025b](https://arxiv.org/html/2608.28639#bib.bib25)\)using three specialized prover models: Goedel\-Prover\-V2\-8B\(Linet al\.[2025c](https://arxiv.org/html/2608.28639#bib.bib15)\), DeepSeek\-Prover\-V2\-7B\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\), and Kimina\-Prover\-Preview\-Distill\-7B\(Wanget al\.[2025](https://arxiv.org/html/2608.28639#bib.bib16)\)\. All results are averaged over 5 random seeds\. Unlike much prior work in this area, we report mean±\\pmstandard deviation across 5 random seeds for all experiments to support statistical reliability of the reported gains\.

#### Baseline description

BFS\+CG\. Breadth\-first expansion of the decomposition tree in which the critic score alone ranks and selects nodes for expansion at each level, with no UCB criterion and no backpropagation of compiler reward along the search path\.

One\-shot decomposition\. All 16 subgoal candidates are generated in a single flat expansion from the root and each is evaluated independently, with no iterative reselection isolating whether gains derive from decomposition scaffolding alone rather than from iterative, reward\-guided search\.

Both baselines use the identical frozen checkpoints for the generator, decomposer, and critic roles as our framework, and identical prompt templates and decoding configurations; they differ from our method only in the search mechanism that allocates the fixed proof\-attempt budget\.

### Main Results

Table[2](https://arxiv.org/html/2608.28639#Sx4.T2)and[3](https://arxiv.org/html/2608.28639#Sx4.T3)reports results on MiniF2F test set\. Our method consistently outperforms whole proof sampling methods across all three models at matched proof attempt budgets\. On Goedel\-Prover\-V2\-8B our method achieves84\.2±0\.5%\\mathbf\{84\.2\\pm 0\.5\\%\}at PAB@32, surpassing whole\-proof baseline \(82\.4%82\.4\\%\) \(Table[3](https://arxiv.org/html/2608.28639#Sx4.T3)\)\. To analyze the importance of individual reward functions, we perform ablations comparing the critic\-only reward against the combined critic \+ verifier reward \(Table[4](https://arxiv.org/html/2608.28639#Sx4.T4)\)\.

To directly compare against a feedback\-driven baseline on the same checkpoint, we reproduce Prover Agent\(Babaet al\.[2026](https://arxiv.org/html/2608.28639#bib.bib18)\)using their released implementation with Goedel\-Prover\-V2\-8B as the prover model, under our evaluation environment \(Lean 4\.15\.0, Mathlib commit 9837ca9d\)\. At their native sample budget of 260, we obtain86\.2±0\.1%\\mathbf\{86\.2\\pm 0\.1\\%\}on MiniF2F, compared to87\.1±0\.2%\\mathbf\{87\.1\\pm 0\.2\\%\}for our method at PAB@256, despite Prover Agent’s use of direct compiler\-error feedback in context versus our oracle\-only signal\.

On PutnamBench \(Table[5](https://arxiv.org/html/2608.28639#Sx4.T5)\), our method solves26/65926/659problems with Goedel\-Prover\-V2\-8B at PAB@32 and36/65936/659at PAB@128, compared to18/65918/659and22/65922/659for whole\-proof sampling\. On PhysLeandata and LeanPhysBench \(Tables[6](https://arxiv.org/html/2608.28639#Sx4.T6),[7](https://arxiv.org/html/2608.28639#Sx4.T7)\), our method consistently outperforms whole\-proof sampling across all three models at the matched budget of PAB@16, with gains of\+1\.9%\+1\.9\\%to\+2\.4%\+2\.4\\%on PhysLeandata and\+1\.5%\+1\.5\\%to\+2\.0%\+2\.0\\%on LeanPhysBench with PhysLib context\. Notably, our method without PhysLib context approaches the performance of whole\-proof sampling with PhysLib suggesting that structured search partially compensates for the absence of domain\-specific library context\. Consistent gains across both physics benchmarks demonstrate that our method generalizes beyond mathematical domains where model familiarity is minimal\.

## Inference\-token efficiency

In this section we additionally compare cumulative inference\-token usage at PAB@32 \(Table[8](https://arxiv.org/html/2608.28639#Sx6.T8)\)\. All reported counts are averaged across five complete runs per sample\. We use vLLM package for inference with one model instance loaded per GPU; the same instance serves the generator, decomposer, and critic roles\. We use 4 Nvidia H200\-SXM GPUs for inference\. Multiple completions are generated within batched requests: whole\-proof sampling produces 32 outputs from one request, while each critic evaluation produces five outputs in one request whose scores are subsequently averaged\. To ensure strict budget matching, neither method terminates early after finding a valid proof\.

Despite the additional decomposition and critic computations, our framework consistently consumes fewer inference tokens across all three models\. Relative to whole\-proof sampling, total token usage decreases by 32\.29% for Goedel\-Prover\-V2\-8B, 33\.17% for DeepSeek\-Prover\-V2\-7B, and 33\.07% for Kimina\-Prover\-7B\. Output\-token usage decreases by 35\.35%, 36\.07%, and 36\.05%, respectively\. Averaged across the three models, our framework reduces output\-token generation by 35\.83% and total token consumption by 32\.84%\. These results show that the short decomposer and critic interactions substantially reduce the number of generator output tokens consumed under the same proof\-attempt budget, more than offsetting their additional token overhead\. Both methods use an identical vLLM deployment with one model instance per GPU and the same maximum GPU\-memory\-utilisation setting of 0\.95\.

Table 8:Role\-level inference\-token usage at PAB@32, averaged across five runs\. Token counts are cumulative across all role completions in one complete benchmark run\.ModelRole/MethodInputOutputTotalGoedel\-Prover\-V2\-8BDecomposer1,4381,4492,887Critic4,1261964,322Generator4,231203,580207,811Whole\-proof117317,420317,537DeepSeek\-Prover\-V2\-7BDecomposer1,3471,3922,739Critic4,0211874,208Generator4,058204,113208,171Whole\-proof117321,762321,879Kimina\-Prover\-7BDecomposer1,4271,4662,893Critic4,0831854,268Generator4,135203,611207,746Whole\-proof117320,986321,103### Effect of Adaptive Decomposer Temperature

Table[9](https://arxiv.org/html/2608.28639#Sx6.T9)reports the effect of removing temperature decay from the decomposer, replacing the annealed schedule

τd=τ0⋅e−0\.12​d⋅e−0\.03​ln⁡\(1\+i\)\\tau\_\{d\}\\;=\\;\\tau\_\{0\}\\cdot e^\{\-0\.12\\,d\}\\cdot e^\{\-0\.03\\ln\(1\+i\)\}\(4\)
\(Equation[4](https://arxiv.org/html/2608.28639#Sx6.E4)\) with a fixed temperature ofτ=0\.7\\tau\{=\}0\.7throughout\. Removing temperature decay consistently degrades performance across all three models: Kimina\-Prover\-7B drops from64\.3±0\.8%64\.3\\pm 0\.8\\%to62\.5±0\.5%62\.5\\pm 0\.5\\%\(−1\.8%\-1\.8\\%\), DeepSeek\-Prover\-V2\-7B from77\.1±0\.3%77\.1\\pm 0\.3\\%to74\.6±0\.3%74\.6\\pm 0\.3\\%\(−2\.5%\-2\.5\\%\), and Goedel\-Prover\-V2\-8B from84\.2±0\.5%84\.2\\pm 0\.5\\%to81\.9±0\.3%81\.9\\pm 0\.3\\%\(−2\.3%\-2\.3\\%\)\.

These consistent drops across all models confirm that temperature decay is a critical architectural component rather than a model\-specific artifact\. Without decay, the decomposer maintains high temperature throughout the search continuing to propose diverse subgoals even at deeper depths and later iterations where the search should be committing to promising proof directions\. This prevents the tree from effectively exploiting high\-reward subtrees identified by backpropagated compiler rewards, reducing the search to essentially diverse but unguided sampling\.

Table 9:Results with and without temperature variation on miniF2F test set \(proof attempt budget = 32; critic \+ server rewards used for all configurations\)\. Results are averaged across 5 random seeds\.ModelMethodSuccess \(%\)KiminaAgent \(ours, w/ temp\. variation\)64\.3±0\.8\\mathbf\{64\.3\\pm 0\.8\}Agent \(ours, w/o temp\. variation\)62\.5±0\.562\.5\\pm 0\.5DeepSeekAgent \(ours, w/ temp\. variation\)77\.1±0\.3\\mathbf\{77\.1\\pm 0\.3\}Agent \(ours, w/o temp\. variation\)74\.6±0\.374\.6\\pm 0\.3GoedelAgent \(ours, w/ temp\. variation\)84\.2±0\.5\\mathbf\{84\.2\\pm 0\.5\}Agent \(ours, w/o temp\. variation\)81\.9±0\.381\.9\\pm 0\.3
### Multi\-Agent Role Analysis

Table[10](https://arxiv.org/html/2608.28639#Sx6.T10)reports results from our systematic multi\-agent analysis on Minif2f test set for proof attempt budget of 32 \(PAB@32\), where Goedel\-Prover\-V2\-8B is fixed as the generator and all combinations of Goedel\-Prover\-V2\-8B, DeepSeek\-Prover\-V2\-7B, and Kimina\-Prover\-7B are evaluated in the decomposer and critic roles\. The objective is to examine whether introducing heterogeneous models into supporting roles can improve proof search performance over the homogeneous baseline\.

Among the evaluated critic assignments, heterogeneous critics exhibit mixed behavior\. Using DeepSeek\-Prover\-V2\-7B as the critic achieves the best overall performance \(86\.1±0\.3%\\mathbf\{86\.1\\pm 0\.3\\%\}\), improving upon the homogeneous configuration \(84\.2±0\.5%84\.2\\pm 0\.5\\%\) by1\.91\.9percentage points\. In contrast, replacing the critic with Kimina\-Prover\-7B decreases performance to82\.7±0\.4%82\.7\\pm 0\.4\\%\. These results indicate that, for the models evaluated here, an appropriately chosen heterogeneous critic can provide complementary evaluation signals that improve search quality, although this benefit is not observed for every model substitution\.

The decomposer role exhibits a different trend\. Replacing the homogeneous Goedel\-Prover\-V2\-8B decomposer with either DeepSeek\-Prover\-V2\-7B or Kimina\-Prover\-7B consistently reduces performance, achieving83\.8±0\.4%83\.8\\pm 0\.4\\%\(−0\.4\-0\.4points\) and82\.2±0\.5%82\.2\\pm 0\.5\\%\(−2\.0\-2\.0points\), respectively\. Furthermore, combining heterogeneous models in both supporting roles does not preserve the critic improvement\. For example, using DeepSeek\-Prover\-V2\-7B as both decomposer and critic achieves only80\.9±0\.3%80\.9\\pm 0\.3\\%, substantially below both the homogeneous baseline \(84\.2±0\.5%84\.2\\pm 0\.5\\%\) and the configuration that changes only the critic \(86\.1±0\.3%86\.1\\pm 0\.3\\%\)\. This suggests that, for the evaluated models, the performance gain from a heterogeneous critic depends on maintaining a homogeneous generator–decomposer pair\.

Overall, within the scope of the evaluated models and benchmark, the strongest configuration pairs a Goedel\-Prover\-V2\-8B generator and decomposer with a DeepSeek\-Prover\-V2\-7B critic\. These findings suggest that selectively introducing heterogeneity into the critic role is a promising direction for improving theorem\-proving search, while additional experiments across a broader range of generator models and benchmarks are needed to determine the extent to which these observations generalize\.

Table 10:Multi\-agent analysis with different models in different roles on miniF2F test set with sampling budget PAB@32\. Results are averaged across 5 random seeds\.GeneratorDecomposerCriticSuccess \(%\)GoedelKiminaKimina81\.4±0\.481\.4\\pm 0\.4GoedelKiminaGoedel82\.2±0\.582\.2\\pm 0\.5GoedelGoedelKimina82\.7±0\.482\.7\\pm 0\.4GoedelDeepSeekDeepSeek80\.9±0\.380\.9\\pm 0\.3GoedelGoedelDeepSeek86\.1±0\.3\\mathbf\{86\.1\\pm 0\.3\}GoedelDeepSeekGoedel83\.8±0\.483\.8\\pm 0\.4GoedelGoedelGoedel84\.2±0\.584\.2\\pm 0\.5†
†Baseline\.

### Effect of the Iteration–Branching Allocation

We study how the fixed proof\-attempt budget should be distributed between the number of MCTS iterationsNNand the branching factorKK\. We keep the number of complete proof attempts per child fixed atS=2S=2and varyNNandKKsuch that

N×K×S=32N\\times K\\times S=32for every configuration\. Consequently, all settings use the same maximum number of complete proof generations, decomposition calls, and critic evaluations\. Specifically, each configuration producesN​K=16NK=16decomposition candidates,5​N​K=805NK=80critic evaluations, andN​K​S=32NKS=32complete proof attempts\. The configurations therefore differ primarily in how these calls are distributed across sequential MCTS iterations\.

Table 11:Effect of the iteration–branching\-factor allocation under a fixed proof\-attempt budget on MiniF2F with Goedel\-Prover\-V2\-8B\. We fixS=2S=2proof attempts per child and vary the number of MCTS iterationsNNand children per expansionKK, such thatN​K​S=32NKS=32for all configurations\. Wall\-clock time is reported relative to theN=1,K=16N=1,K=16configuration\. Results are averaged over five random seeds\.NNKKSSSuccess \(%\)Rel\. Wall\-Clock116282\.1±0\.482\.1\\pm 0\.41\.0×1\.0\\times28282\.3±0\.382\.3\\pm 0\.31\.2×1\.2\\times4†4284\.2±0\.5\\mathbf\{84\.2\\pm 0\.5\}1\.5×1\.5\\times82283\.7±0\.483\.7\\pm 0\.42\.1×2\.1\\times161284\.3±0\.284\.3\\pm 0\.22\.8×2\.8\\times
†Configuration used in our main results\.

As shown in Table[11](https://arxiv.org/html/2608.28639#Sx6.T11), shallow configurations with large branching factors are computationally efficient but achieve lower proof success\. TheN=1,K=16N=1,K=16andN=2,K=8N=2,K=8configurations obtain success rates of82\.1%82\.1\\%and82\.3%82\.3\\%, respectively\. In these settings, most of the budget is allocated to generating a broad set of decompositions, with limited opportunity to use intermediate rewards to guide subsequent node selection\.

Increasing the number of MCTS iterations toN=4N=4improves success to84\.2%84\.2\\%\. Notably, theN=1,K=16N=1,K=16andN=4,K=4N=4,K=4configurations use the same numbers of decomposition calls, critic evaluations, and complete proof attempts\. Their performance difference therefore cannot be attributed to a larger component\-call budget\. Instead, the result indicates that distributing node expansions across multiple MCTS iterations, with intermediate reward backpropagation and subsequent UCB\-guided selection, is more effective than generating all decomposition candidates in a single expansion\.

Further increasing the number of iterations produces diminishing returns\. TheN=8,K=2N=8,K=2configuration achieves83\.7%83\.7\\%, while the narrowest configuration,N=16,K=1N=16,K=1, achieves84\.3%84\.3\\%\. The latter is only0\.10\.1percentage points above theN=4,K=4N=4,K=4configuration, while requiring2\.8×2\.8\\timesthe wall\-clock time of theN=1,K=16N=1,K=16setting, compared with1\.5×1\.5\\timesforN=4,K=4N=4,K=4\. This difference in success is small relative to the variation across random seeds\.

These results reveal an accuracy–latency trade\-off\. Broad, shallow search reduces inference latency but provides insufficient iterative refinement, whereas very narrow search increases sequential search overhead without yielding a meaningful improvement in proof success\. We therefore useN=4,K=4,S=2N=4,K=4,S=2in the main experiments, as it provides the best practical balance between proof success and wall\-clock efficiency under the fixed proof\-attempt budget\.

#### Reward Hacking Analysis\.

DeepSeek\-Prover\-V2\-7B exhibits a substantially different pattern on PutnamBench\. Before exploit auditing, whole\-proof sampling solves13/65913/659problems at PAB@32 and18/65918/659at PAB@128, whereas our method solves27/65927/659and44/65944/659, respectively\. However, screening the successful proofs using previously reported exploit indicators identifies a substantial number containing theapply?tactic and Cardinal\-family lemmas \(Cardinal\.toNat,Cardinal\.natCast\_inj\)\. These patterns were identified in the DeepSeek\-Prover\-V2\-7B technical report\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\)as being associated with a Lean 4\.9\.0 compiler/interface vulnerability in whichapply?may fail to emit an explicitsorrydeclaration under certain conditions, producing proof declarations that compile despite depending onsorryAx\.

After excluding proofs confirmed by our audit to depend onsorryAx, the whole\-proof solve counts decrease from13/65913/659to9/6599/659at PAB@32 and from18/65918/659to10/65910/659at PAB@128\. Thus, the audit removes 4 and 8 whole\-proof solutions at the two budgets\. For our method, the solve counts decrease from27/65927/659to16/65916/659at PAB@32 and from44/65944/659to25/65925/659at PAB@128, removing 11 and 19 solutions, respectively\. Consequently, our method produces 7 more exploit\-dependent successful proofs than whole\-proof sampling at PAB@32 and 11 more at PAB@128\.

Critically, successful exploitation is not observed on the physics benchmarks\. On PhysLeandata, DeepSeek\-Prover\-V2\-7B generates exploit\-related patterns for only 1 of the 200 evaluated problems, and none of these attempts compile successfully\. Likewise, no exploit\-dependent successful proof is identified on LeanPhysBench\. These results suggest that the prover lacks sufficient familiarity with the graduate\-level physics formalizations to construct the surrounding Lean context required for the documented exploit pattern to succeed\. We therefore observe successful exploit\-dependent proofs primarily on PutnamBench, where the underlying prover already exhibits the documented behaviour\. We report both unaudited and audited results transparently in Table[5](https://arxiv.org/html/2608.28639#Sx4.T5)and recommend kernel\-level proof auditing for models that exhibit anomalous increases in compiler\-verified solve counts under search\-based inference\.

#### Potential Exploit Identification\.

To investigate the generation of exploitative proof strategies, we adopt a conservative multi\-stage audit protocol\. We first identify*potentially suspicious*proof attempts using the exploit patterns reported in the DeepSeek\-Prover\-V2\-7B technical report\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\)\. That work reports that the 7B model occasionally exploits a Lean 4\.9\.0 compiler/interface bug on PutnamBench through characteristic proof structures involving theapply?tactic together with specificCardinal\-related lemmas, includingCardinal\.toNatandCardinal\.natCast\_inj\. We use these patterns only as an initial screening mechanism; their lexical presence is never treated as sufficient evidence that a proof is exploitative\. Because we are not Lean 4 domain experts, we rely on the indicators documented in prior work rather than independently deriving new exploit signatures\. Accordingly, our initial screening can detect recurrences of the documented exploit family but cannot by itself rule out undocumented exploit patterns\.

For every successfully compiled proof, including proofs that do not contain the previously reported lexical indicators, we append\#print axioms <theorem\_name\>and recompile the resulting code using the same Lean evaluation environment\. A proof is classified as a*potential exploit*only when the resulting theorem declaration depends onsorryAx\. For proofs that also contain a documented suspicious construction, we additionally remove that construction and verify that the proof no longer compiles\. Thus, neither the presence ofapply?nor the use of Cardinal\-family lemmas is independently sufficient for classification\. Only successful proofs whose resulting declarations depend onsorryAxare removed from the audited solve counts\. Since the underlying Lean behaviour has already been documented in prior work\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\), we use the term*potential exploit*rather than claiming to have independently established a new compiler vulnerability\.

Across all experiments, successful exploit\-dependent proofs are observed only for DeepSeek\-Prover\-V2\-7B on PutnamBench\. Under whole\-proof sampling, the audit removes 4 successful proofs at PAB@32 and 8 at PAB@128\. Under our MCTS framework, it removes 11 successful proofs at PAB@32 and 19 at PAB@128\. No successful proof generated by Goedel\-Prover\-V2\-8B or Kimina\-Prover\-Preview\-Distill\-7B is found to depend onsorryAxunder the same audit protocol\. Although DeepSeek\-Prover\-V2\-7B occasionally generates proof attempts containing exploit\-related patterns on PhysLeandata, LeanPhysBench, and the MiniF2F test set, none of these attempts both compile successfully and produce a theorem declaration depending onsorryAx\. They therefore do not contribute to the reported solve counts\. These observations suggest that our MCTS framework does not introduce a new exploit strategy; instead, it could increase the number of successful exploit\-dependent proofs produced by a model that already exhibits the documented behavior\.

All our experiments, including the baselines, are conducted using Lean 4\.15\.0, Mathlib v4\.15\.0 \(commit9837ca9d, dated 2025\-01\-05\), and the Kimina Lean Server 2\.0\.0 container image\. Although the underlying interface behavior was originally documented under Lean 4\.9\.0\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\), we verify that proof attempts exhibiting the documentedapply?\-based pattern continue to produce theorem declarations depending onsorryAxunder our pinned Lean 4\.15\.0 and Mathlib environment\.

To ensure that the audit is not limited to proofs matching the previously reported lexical indicators, we execute\#print axiomson every successfully compiled proof generated by all three prover models, across all four benchmarks, methods, and proof\-attempt budgets\. Because\#print axiomsqueries the dependencies of the resulting Lean declaration rather than relying on the evaluation wrapper’s surface\-level compilation status or source\-levelsorryscan, it directly determines whether a successful declaration depends on kernel axioms such assorryAx\. This exhaustive audit finds nosorryAxdependency among successful proofs generated by Goedel\-Prover\-V2\-8B or Kimina\-Prover\-Preview\-Distill\-7B under any evaluated configuration\.

The same audit procedure is applied uniformly to whole\-proof sampling and MCTS\-generated proofs, enabling a controlled comparison between the two inference procedures\. We emphasize that this procedure verifies axiom\-level dependencies as reported by Lean; it does not constitute an independent mathematical or semantic validation beyond the guarantees provided by Lean’s kernel and axiom\-dependency tracking\.

## Implementation details

#### Reproduction protocol and comparability to published results

\. All baselines in the paper are re\-run in\-house under a single pinned environment \(Lean 4\.15\.0, Mathlib v4\.15\.0 commit 9837ca9d dated 2025\-01\-05, Kimina Lean Server 2\.0\.0\), using the prompt templates in Section[Prompt Configurations](https://arxiv.org/html/2608.28639#Sx7.SSx2)and the decoding configurations in Section[Inference configuration\.](https://arxiv.org/html/2608.28639#Sx7.SSx1)\. Our whole\-proof sampling numbers are consequently not directly comparable to the pass@k figures reported in the original model releases, and we do not present them as reproductions of those figures\. The factors accounting for the difference are, first, published numbers are obtained under substantially older toolchain pins, and solve rates are highly sensitive to this choice:\(Guet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib46)\)measure the same Goedel\-Prover\-V2\-32B checkpoint at 90% pass@64 on MiniF2F and 86 solves on PutnamBench at pass@184 under Mathlib 4\.9, but at 80% and 75 solves respectively under Mathlib 4\.19 a ten\-point swing on MiniF2F attributable to the toolchain alone, with no change to the model\. Second, published figures use model\-specific prompt templates and, for Goedel\-Prover\-V2, an optional compiler\-guided self\-correction mode; we instead use one uniform prompt template and decoding configuration across all three provers and disable self\-correction, so that every method under comparison differs only in its search procedure and not in its inference stack\.

Our decision to pin a recent toolchain rather than reproduce the original evaluation environment is deliberate\. The axiom\-level audit in the main paper \(Subsections: Reward Hacking Analysis, Potential Exploit Identification\) shows that the Lean 4\.9\.0\-era interface behaviour documented by\(Renet al\.[2025](https://arxiv.org/html/2608.28639#bib.bib17)\)admits proof declarations that compile successfully, pass the standard source\-level sorry scan, and nonetheless depend on sorryAx\. Compiler\-verified solve counts obtained under that toolchain therefore cannot be taken at face value without a kernel\-level audit, and re\-deriving every baseline within a single pinned and exhaustively audited environment is what makes the internal comparisons in this paper meaningful\. Every result reported in the main paper whole\-proof sampling, BFS\+CG, one\-shot decomposition, our reproduction of Prover Agent, and our framework is internal to this environment, uses identical frozen checkpoints, and varies only the inference\-time procedure\.

#### Physlib library

PhysLib is a Lean 4 support library introduced alongside LeanPhysBench in Lean4Physics\(Liet al\.[2025b](https://arxiv.org/html/2608.28639#bib.bib25)\)\. It formalizes standard physical units, dimensional constants, and the associated definitions against which the benchmark’s theorem statements are written\. Following the evaluation protocol of\(Liet al\.[2025b](https://arxiv.org/html/2608.28639#bib.bib25)\), we supply PhysLib as direct input context: the library is prepended to the theorem statement within the prompt, rather than being exposed through premise retrieval or an import mechanism\.

We report LeanPhysBench results both with and without this context Table[7](https://arxiv.org/html/2608.28639#Sx4.T7)\. The with\-PhysLib condition matches the setting used in the original benchmark evaluation and is the primary comparison; the no\-PhysLib condition measures how far a prover can proceed on physics formalizations without access to the domain\-specific definitions its statements depend on\. The protocol is applied identically to whole\-proof sampling and to our framework at every budget, so the with/without contrast varies only the presence of library context\.

### Inference configuration\.

The three agent roles use different decoding configurations tailored to their respective objectives\.

- •Generator\.Maximum generation length is 16,384 tokens with decoding temperatureτ=0\.7\\tau=0\.7\. This relatively higher temperature encourages diverse proof attempts while remaining sufficiently stable for formal proof generation\.
- •Decomposer\.Maximum generation length is 1,024 tokens\. The decomposer uses the adaptive temperature schedule described in Equation[4](https://arxiv.org/html/2608.28639#Sx6.E4), allowing broader exploration during early search and progressively more focused subgoal generation at deeper levels\.
- •Critic\.Maximum generation length is limited to 3 tokens with decoding temperatureτ=0\.3\\tau=0\.3\. Since the critic produces only scalar quality ratings rather than proofs, a low temperature is used to obtain stable and reproducible evaluations\.

### Prompt Configurations

We report the exact system prompts used for each of the three agent roles below\. The same prompt template is used across all three prover models \(Goedel\-Prover\-V2\-8B, DeepSeek\-Prover\-V2\-7B, Kimina\-Prover\-7B\) and all four benchmarks \(MiniF2F, PutnamBench, PhysLeandata, LeanPhysBench\); only the theorem statement, decomposition trajectory, and \(where applicable\) domain\-specific library context are substituted into the template placeholders at inference time\.

Generator System Prompt[⬇](data:text/plain;base64,WW91IGFyZSBhbiBleHBlcnQgTGVhbjQgdGhlb3JlbSBwcm92ZXIuCkdpdmVuIGEgdGhlb3JlbSBhbmQgYSBkZWNvbXBvc2l0aW9uIHRoYXQgYnJlYWtzIGl0IGludG8gdHJhY3RhYmxlIHN0ZXBzLCBwcm9kdWNlIGEgY29tcGxldGUgTGVhbjQgcHJvb2YuCgpUSEVPUkVNOgp7dGhlb3JlbX0KCkRFQ09NUE9TSVRJT046CntkZWNvbXBvc2l0aW9ufQoKSU5TVFJVQ1RJT05TOgotIFlvdSBtYXkgdXNlIGEgPHRoaW5rPi4uLjwvdGhpbms+IGJsb2NrIGZvciBpbnRlcm5hbCByZWFzb25pbmcKLSBBZnRlciB0aGUgdGhpbmtpbmcgYmxvY2ssIG91dHB1dCBPTkxZIHRoZSByYXcgTGVhbjQgcHJvb2YsIG5vIG1hcmtkb3duIGZlbmNlcywgbm8gcHJvc2UKLSBTdGFydCB5b3VyIExlYW40IG91dHB1dCBkaXJlY3RseSB3aXRoIHRoZSB0aGVvcmVtIGRlY2xhcmF0aW9uIG9yIGBieWAKLSBVc2UgYGhhdmVgIHN0YXRlbWVudHMgdG8gZW5jb2RlIGVhY2ggZGVjb21wb3NpdGlvbiBzdGVwIGFzIGFuIGludGVybWVkaWF0ZSBnb2FsCi0gVGhlIHByb29mIG11c3QgdHlwZWNoZWNrIGFuZCBjbG9zZSBhbGwgZ29hbHMKLSBEbyBub3Qgb3V0cHV0IGFueXRoaW5nIGFmdGVyIHRoZSBjbG9zaW5nIGBkb25lYCBvciBmaW5hbCB0YWN0aWM=)1YouareanexpertLean4theoremprover\.2Givenatheoremandadecompositionthatbreaksitintotractablesteps,produceacompleteLean4proof\.34THEOREM:5\{theorem\}67DECOMPOSITION:8\{decomposition\}910INSTRUCTIONS:11\-Youmayusea<think\>\.\.\.</think\>blockforinternalreasoning12\-Afterthethinkingblock,outputONLYtherawLean4proof,nomarkdownfences,noprose13\-StartyourLean4outputdirectlywiththetheoremdeclarationor‘by‘14\-Use‘have‘statementstoencodeeachdecompositionstepasanintermediategoal15\-Theproofmusttypecheckandcloseallgoals16\-Donotoutputanythingaftertheclosing‘done‘orfinaltactic

Critic System Prompt[⬇](data:text/plain;base64,WW91IGFyZSBhbiBleHBlcnQgTGVhbjQgdGhlb3JlbSBwcm92aW5nIGV2YWx1YXRvci4KWW91IHdpbGwgYmUgZ2l2ZW46CjEuIEEgbWFpbiBMZWFuNCB0aGVvcmVtIHRvIHByb3ZlCjIuIEEgZGVjb21wb3NpdGlvbiB0cmFqZWN0b3J5IG9mIHByaW9yIHN0ZXBzIChpZiBhbnkpCjMuIEEgY2FuZGlkYXRlIG5leHQgZGVjb21wb3NpdGlvbiBzdGVwIHRvIGV2YWx1YXRlCgpSYXRlIHRoZSBjYW5kaWRhdGUgc3RlcCBvbiBob3cgdXNlZnVsIGl0IGlzIGZvciBtYWtpbmcgdGhlIG1haW4gdGhlb3JlbSBwcm92YWJsZS4KClNjb3JpbmcgY3JpdGVyaWE6Ci0gRG9lcyBpdCBtZWFuaW5nZnVsbHkgcmVkdWNlIHRoZSBwcm9vZiBidXJkZW4gb2YgdGhlIG1haW4gdGhlb3JlbT8gKDAtMjUgcHRzKQotIElzIGl0IGNvbnNpc3RlbnQgd2l0aCBhbmQgYnVpbGRzIG9uIHRoZSBwcmlvciB0cmFqZWN0b3J5PyAoMC0yNSBwdHMpCi0gSXMgaXQgc3BlY2lmaWMgYW5kIGltbWVkaWF0ZWx5IGFjdGlvbmFibGUgaW4gTGVhbjQ/ICgwLTI1IHB0cykKLSBEb2VzIGl0IGF2b2lkIHJlZHVuZGFuY3kgd2l0aCBwcmlvciBzdGVwcz8gKDAtMjUgcHRzKQoKU2NvcmUgYW5jaG9yczoKLSAwLTIwOiBJcnJlbGV2YW50LCB3cm9uZyBkaXJlY3Rpb24sIG9yIGhhcm1mdWwgdG8gdGhlIHByb29mCi0gMjEtNDA6IFZhZ3VlbHkgcmVsYXRlZCBidXQgbm90IGFjdGlvbmFibGUKLSA0MS02MDogUmVhc29uYWJsZSBidXQgZ2VuZXJpYyBvciBwYXJ0aWFsbHkgdXNlZnVsCi0gNjEtODA6IENsZWFybHkgdXNlZnVsIGFuZCBkaXJlY3RseSByZWR1Y2VzIHByb29mIGJ1cmRlbgotIDgxLTEwMDogT3B0aW1hbCBuZXh0IHN0ZXAsIHByZWNpc2UgYW5kIGltbWVkaWF0ZWx5IGFjdGlvbmFibGUKClRoZW9yZW06IHt0aGVvcmVtfQpUcmFqZWN0b3J5OiB7dHJhamVjdG9yeX0KQ2FuZGlkYXRlIHN0ZXA6IHtjYW5kaWRhdGVfc3RlcH0KU2NvcmU6)1YouareanexpertLean4theoremprovingevaluator\.2Youwillbegiven:31\.AmainLean4theoremtoprove42\.Adecompositiontrajectoryofpriorsteps\(ifany\)53\.Acandidatenextdecompositionsteptoevaluate67Ratethecandidatesteponhowusefulitisformakingthemaintheoremprovable\.89Scoringcriteria:10\-Doesitmeaningfullyreducetheproofburdenofthemaintheorem?\(0\-25pts\)11\-Isitconsistentwithandbuildsonthepriortrajectory?\(0\-25pts\)12\-IsitspecificandimmediatelyactionableinLean4?\(0\-25pts\)13\-Doesitavoidredundancywithpriorsteps?\(0\-25pts\)1415Scoreanchors:16\-0\-20:Irrelevant,wrongdirection,orharmfultotheproof17\-21\-40:Vaguelyrelatedbutnotactionable18\-41\-60:Reasonablebutgenericorpartiallyuseful19\-61\-80:Clearlyusefulanddirectlyreducesproofburden20\-81\-100:Optimalnextstep,preciseandimmediatelyactionable2122Theorem:\{theorem\}23Trajectory:\{trajectory\}24Candidatestep:\{candidate\_step\}25Score:

Decomposer Prompt[⬇](data:text/plain;base64,WW91IGFyZSBhbiBleHBlcnQgTGVhbjQgcHJvb2Ygc3RyYXRlZ2lzdC4KWW91IHdpbGwgYmUgZ2l2ZW4gYSB0aGVvcmVtIGFuZCBvcHRpb25hbGx5IGEgbGlzdCBvZiBkZWNvbXBvc2l0aW9uIHN0ZXBzIGFscmVhZHkgcGxhbm5lZC4KWW91ciB0YXNrIGlzIHRvIG91dHB1dCB0aGUgc2luZ2xlIG1vc3QgdXNlZnVsIE5FWFQgcHJvb2Ygc3RlcC4KClRIRU9SRU06Cnt0aGVvcmVtfQp7cHJpb3Jfc3RlcHNfYmxvY2t9CgpJTlNUUlVDVElPTlM6Ci0gT3V0cHV0IEVYQUNUTFkgT05FIG5leHQgc3RlcCwgb25lIHNlbnRlbmNlLCBwbGFpbiBFbmdsaXNoCi0gVGhlIHN0ZXAgbXVzdCBiZSBhIGNvbmNyZXRlIHByb29mLXN0cnVjdHVyYWwgbW92ZTogYW4gaW5kdWN0aW9uIHNjaGVtZSwgYSBjYXNlIHNwbGl0LAogIGEga2V5IGxlbW1hIHRvIGVzdGFibGlzaCwgYSByZXdyaXRlIHJ1bGUgdG8gYXBwbHksIG9yIGFuIGFsZ2VicmFpYyB0cmFuc2Zvcm1hdGlvbgotIEl0IG11c3QgZGlyZWN0bHkgcmVkdWNlIHdoYXQgcmVtYWlucyB0byBiZSBwcm92ZW4KLSBEbyBOT1Qgd3JpdGUgTGVhbjQgY29kZSBvciBwc2V1ZG9jb2RlCi0gRG8gTk9UIGV4cGxhaW4geW91ciByZWFzb25pbmcKLSBEbyBOT1QgcmVwZWF0IHByaW9yIHN0ZXBzCi0gRG8gTk9UIHN0YXRlIHdoYXQgdGhlIGZpbmFsIGFuc3dlciBpcwoKVmFsaWQgZXhhbXBsZXM6CiAgIkFwcGx5IGluZHVjdGlvbiBvbiBuLCBoYW5kbGluZyB0aGUgYmFzZSBjYXNlIG49MCBhbmQgc3RlcCBjYXNlIHNlcGFyYXRlbHkuIgogICJSZXdyaXRlIHRoZSBnb2FsIHVzaW5nIHRoZSBpZGVudGl0eSBhXjIgLSBiXjIgPSAoYS1iKShhK2IpLiIKICAiQ2FzZSBzcGxpdCBvbiB3aGV0aGVyIGsgaXMgZXZlbiBvciBvZGQuIgogICJFc3RhYmxpc2ggdGhlIGF1eGlsaWFyeSBsZW1tYSB0aGF0IGYobikgaXMgbW9ub3RvbmUgaW5jcmVhc2luZywgdGhlbiBhcHBseSBpdCB0byBib3VuZCB0aGUgc3VtLiIKICAiUmVkdWNlIHRvIHNob3dpbmcgZGl2aXNpYmlsaXR5IGJ5IGV4cHJlc3NpbmcgdGhlIGxlZnQgc2lkZSBhcyBhIHRlbGVzY29waW5nIHByb2R1Y3QuIgoKTmV4dCBzdGVwOg==)1YouareanexpertLean4proofstrategist\.2Youwillbegivenatheoremandoptionallyalistofdecompositionstepsalreadyplanned\.3YourtaskistooutputthesinglemostusefulNEXTproofstep\.45THEOREM:6\{theorem\}7\{prior\_steps\_block\}89INSTRUCTIONS:10\-OutputEXACTLYONEnextstep,onesentence,plainEnglish11\-Thestepmustbeaconcreteproof\-structuralmove:aninductionscheme,acasesplit,12akeylemmatoestablish,arewriteruletoapply,oranalgebraictransformation13\-Itmustdirectlyreducewhatremainstobeproven14\-DoNOTwriteLean4codeorpseudocode15\-DoNOTexplainyourreasoning16\-DoNOTrepeatpriorsteps17\-DoNOTstatewhatthefinalansweris1819Validexamples:20"Applyinductiononn,handlingthebasecasen=0andstepcaseseparately\."21"Rewritethegoalusingtheidentitya^2\-b^2=\(a\-b\)\(a\+b\)\."22"Casesplitonwhetherkisevenorodd\."23"Establishtheauxiliarylemmathatf\(n\)ismonotoneincreasing,thenapplyittoboundthesum\."24"Reducetoshowingdivisibilitybyexpressingtheleftsideasatelescopingproduct\."2526Nextstep:

### Example: A Potential Compiler Exploit

Listing[1](https://arxiv.org/html/2608.28639#LST1)shows a representativeAgent \(critic\+reward\)proof attempt forputnam\_1997\_b5generated by DeepSeek\-Prover\-V2\-7B that was flagged by our audit protocol \(\(Subsections: Reward Hacking Analysis, Potential Exploit Identification\), stated in the main paper\)\. The proof compiles successfully under the Kimina Lean server and superficially follows a standard structure: a base case \(h\_base\), an inductive step \(h\_inductive\), and a chain of trivialexactforwarding \(h\_main,h\_final\) that gives the appearance of a completed induction\. Critically, however, the inductive step’s proof obligation is discharged not through valid tactics but through a cascade oftryblocks that falls back to theapply?tactic \(highlighted, line[46](https://arxiv.org/html/2608.28639#lstnumberx115)\) whenomegaandsimp\_allfail to close the goal\.

Following our audit protocol, we append an axiom check to the compiled proof:

1\#printaxiomsputnam\_1997\_b5

which returns:

1’putnam\_1997\_b5’dependsonaxioms:\[propext,sorryAx,Classical\.choice,Quot\.sound\]

The presence ofsorryAxconfirms that, despite compiling without an explicitsorrytoken in the source and despite passing the Kimina server’ssorry\-token scan, the proof does not in fact close all goalsapply?silently discharges an unproved obligation via the Lean 4\.9\.0 interface bug documented inRenet al\.\([2025](https://arxiv.org/html/2608.28639#bib.bib17)\), rather than genuinely establishing the inductive step\. Removing the flaggedapply?branch causes the proof to fail to compile, satisfying the second criterion of our audit protocol \(\(Subsections: Reward Hacking Analysis, Potential Exploit Identification\), stated in the main paper\)\) and confirming classification as a potential exploit\.

Listing 1:A DeepSeek\-Prover\-V2\-7B proof attempt forputnam\_1997\_b5flagged as a potential exploit\. Line[46](https://arxiv.org/html/2608.28639#lstnumberx115)shows the fallbackapply?tactic responsible for thesorryAxdependency\.1importMathlib

2deftetration:Nat\-\>Nat\-\>Nat

3\|\_,0=\>1

4\|b,\(m\+1\)=\>b^\(tetrationbm\)

5

6theoremputnam\_1997\_b5

7\(n:Nat\)

8\(hn:n\>=2\)

9:tetration2n===tetration2\(n\-1\)\[MODn\]:=by

10haveh\_base:n=2\-\>tetration2n===tetration2\(n\-1\)\[MODn\]:=by

11introhn2

12rw\[hn2\]

13norm\_num\[tetration,Nat\.ModEq\]

14<;\>decide

15

16haveh\_inductive:forallk\>=2,tetration2k===tetration2\(k\-1\)\[MODk\]

17\-\>tetration2\(k\+1\)===tetration2k\[MOD\(k\+1\)\]:=by

18introkhkh

19haveh1:tetration2\(k\+1\)=2^\(tetration2k\):=by

20rw\[tetration\]

21<;\>simp\[Nat\.add\_comm,Nat\.add\_assoc,Nat\.add\_left\_comm\]

22<;\>inductionk<;\>simp\_all\[tetration,Nat\.pow\_succ\]

23<;\>ring\_nfat\*<;\>omega

24haveh2:tetration2k=2^\(tetration2\(k\-1\)\):=by

25caseskwith

26\|zero=\>contradiction

27\|succk=\>

28caseskwith

29\|zero=\>contradiction

30\|succk=\>

31simp\_all\[tetration\]

32<;\>simp\_all\[tetration,Nat\.pow\_succ\]

33<;\>ring\_nfat\*<;\>omega

34rw\[h1\];rw\[h2\]

35haveh3:\(2:Nat\)^\(2^\(tetration2\(k\-1\)\)\)=2^\(2^\(tetration2\(k\-1\)\)\):=rfl

36haveh4:\(2:Nat\)^\(2^\(tetration2\(k\-1\)\)\)=2^\(2^\(tetration2\(k\-1\)\)\):=rfl

37simp\_all\[Nat\.ModEq,Nat\.ModEq\]

38<;\>\(tryomega\)<;\>

39\(try\{caseskwith

40\|zero=\>contradiction

41\|succk=\>

42caseskwith

43\|zero=\>contradiction

44\|succk=\>simp\_all\[tetration,Nat\.pow\_succ,Nat\.ModEq\]<;\>omega\}\)<;\>

45\(try\{simp\_all\[tetration,Nat\.pow\_succ,Nat\.ModEq\]<;\>omega\}\)<;\>

46\(try\{apply?\}\)

47<;\>omega

48

49haveh\_main:forallk\>=2,tetration2k===tetration2\(k\-1\)\[MODk\]:=by

50introkhk

51induction’hkwithkhkih

52\.norm\_num\[tetration,Nat\.ModEq\]

53\.caseskwith

54\|zero=\>contradiction

55\|succk=\>

56caseskwith

57\|zero=\>norm\_num\[tetration,Nat\.ModEq\]at\*

58\|succk=\>

59haveh1:=h\_inductive\(k\+2\)\(byomega\)ih

60simp\_all\[tetration,Nat\.ModEq\]

61<;\>omega

62

63exacth\_mainnhn

## Datasets

We evaluate our framework on four publicly available Lean 4 theorem\-proving benchmarks spanning competition mathematics and college\- to graduate\-level physics\.

MiniF2F\(Zhenget al\.[2022](https://arxiv.org/html/2608.28639#bib.bib23)\)is a benchmark consisting of 244 test problems formalized in Lean 4\. The problems are derived from international mathematics competitions, including the International Mathematical Olympiad \(IMO\), the American Invitational Mathematics Examination \(AIME\), and related contests\. The benchmark covers a diverse range of mathematical domains, including algebra, number theory, geometry, inequalities, combinatorics, induction, and analysis, making it a standard benchmark for evaluating formal theorem provers\.

PutnamBench\(Tsoukalaset al\.[2024](https://arxiv.org/html/2608.28639#bib.bib24)\)is a collection of formally verified problems compiled from the William Lowell Putnam Mathematical Competition\. It contains challenging undergraduate\-level mathematical theorems spanning algebra, analysis, geometry, combinatorics, number theory, and linear algebra, providing a rigorous benchmark for assessing mathematical reasoning and proof\-generation capabilities\.

LeanPhysBench\(Liet al\.[2025b](https://arxiv.org/html/2608.28639#bib.bib25)\)is a benchmark of formally verified college\-level physics problems written in Lean 4\. The dataset covers multiple introductory and intermediate physics domains, including mechanics, oscillations and waves, electromagnetism, thermodynamics, optics, and related topics\. We evaluate both with and without the accompanying PhysLib context following the benchmark protocol\.

PhysLeanData\(Zhanget al\.[2026](https://arxiv.org/html/2608.28639#bib.bib26)\)is a large\-scale Lean 4 benchmark containing graduate\-level theoretical physics formalizations\. The benchmark includes problems from advanced domains such as classical particle mechanics, classical string theory, relativity, quantum mechanics, quantum field theory, and related areas, providing an out\-of\-distribution evaluation setting for assessing the generalization capability of theorem\-proving systems\.

## Conclusion and Limitations

We present a three\-role MCTS framework that treats the Lean 4 compiler purely as a reward oracle, this prevents compiler\-error content from accumulating in the generation context as search depth increases\. This keeps compiler\-feedback overhead constant with search depth\. Under matched proof\-attempt budgets, our method outperforms whole\-proof sampling across four benchmarks spanning competition mathematics and graduate\-level theoretical physics, reaching 87\.1% on MiniF2F with Goedel\-Prover\-V2\-8B at PAB@256, while consuming 32\.8% fewer total inference tokens on average than the whole\-proof baseline\. Ablations show that both the temperature\-decayed decomposer and the distribution of a fixed budget across multiple MCTS iterations, rather than a single wide expansion, are responsible for these gains\. We also present an exhaustive axiom\-level audit\. We ran\#print axiomson every successfully compiled proof produced by all three prover models across all four benchmarks, methods, and budgets not only on proofs matching previously reported lexical indicators\. This audit shows that a substantial fraction of DeepSeek\-Prover\-V2\-7B’s successes on PutnamBench depend on sorryAx despite compiling cleanly and passing the standard source\-level sorry scan: 4 of 13 and 8 of 18 whole\-proof successes at PAB@32 and PAB@128, and 11 of 27 and 19 of 44 under our framework\. The underlying apply? interface behaviour was documented for Lean 4\.9\.0 by Ren et al\. \(2025\); we confirm it persists under our pinned Lean 4\.15\.0 and Mathlib environment\.

## References

- L\. Aniva, C\. Sun, B\. Miranda, C\. Barrett, and S\. Koyejo \(2024\)Pantograph: a machine\-to\-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4\.External Links:2410\.16429,[Link](https://arxiv.org/abs/2410.16429)Cited by:[Lean 4 Proof Evaluation Infrastructure](https://arxiv.org/html/2608.28639#Sx2.SSx6.p3.1)\.
- K\. Baba, C\. Liu, S\. Kurita, and A\. Sannai \(2026\)Prover agent: an agent\-based framework for formal mathematical proofs\.External Links:2506\.19923,[Link](https://arxiv.org/abs/2506.19923)Cited by:[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1),[Main Results](https://arxiv.org/html/2608.28639#Sx5.SSx1.p2.2)\.
- L\. de Moura and S\. Ullrich \(2021\)The lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings,Berlin, Heidelberg,pp\. 625–635\.External Links:ISBN 978\-3\-030\-79875\-8,[Link](https://doi.org/10.1007/978-3-030-79876-5_37),[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p1.1)\.
- K\. Dong and T\. Ma \(2025\)STP: self\-play llm theorem provers with iterative conjecturing and proving\.External Links:2502\.00212,[Link](https://arxiv.org/abs/2502.00212)Cited by:[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1),[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- X\. Feng, Z\. Wan, M\. Wen, S\. M\. McAleer, Y\. Wen, W\. Zhang, and J\. Wang \(2024\)Alphazero\-like tree\-search can guide large language model decoding and training\.External Links:2309\.17179,[Link](https://arxiv.org/abs/2309.17179)Cited by:[Monte Carlo Tree Search in Language Model Reasoning](https://arxiv.org/html/2608.28639#Sx2.SSx3.p1.1)\.
- E\. First, M\. N\. Rabe, T\. Ringer, and Y\. Brun \(2023\)Baldur: whole\-proof generation and repair with large language models\.External Links:2303\.04910,[Link](https://arxiv.org/abs/2303.04910)Cited by:[Formal Theorem Proving with Large Language Models](https://arxiv.org/html/2608.28639#Sx2.SSx1.p1.1),[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- L\. Gao, J\. Schulman, and J\. Hilton \(2022\)Scaling laws for reward model overoptimization\.External Links:2210\.10760,[Link](https://arxiv.org/abs/2210.10760)Cited by:[Reward Hacking in Reinforcement Learning](https://arxiv.org/html/2608.28639#Sx2.SSx5.p1.1)\.
- F\. Gloeckle, J\. Limperg, G\. Synnaeve, and A\. Hayat \(2024\)ABEL: sample efficient online reinforcement learning for neural theorem proving\.InThe 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24,External Links:[Link](https://openreview.net/forum?id=kk3mSjVCUO)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- A\. Gu, B\. Piotrowski, F\. Gloeckle, K\. Yang, and A\. H\. Markosyan \(2025\)ProofOptimizer: training language models to simplify proofs without human demonstrations\.External Links:2510\.15700,[Link](https://arxiv.org/abs/2510.15700)Cited by:[Reproduction protocol and comparability to published results](https://arxiv.org/html/2608.28639#Sx7.SSx3.SSS0.Px1.p1.1)\.
- S\. Hao, Y\. Gu, H\. Ma, J\. J\. Hong, Z\. Wang, D\. Z\. Wang, and Z\. Hu \(2023\)Reasoning with language model is planning with world model\.External Links:2305\.14992,[Link](https://arxiv.org/abs/2305.14992)Cited by:[Monte Carlo Tree Search in Language Model Reasoning](https://arxiv.org/html/2608.28639#Sx2.SSx3.p1.1)\.
- X\. Ji, Y\. Liu, Q\. Wang, J\. Zhang, Y\. Yue, R\. Shi, C\. Sun, F\. Zhang, G\. Zhou, and K\. Gai \(2025\)Leanabell\-prover\-v2: verifier\-integrated reasoning for formal theorem proving via reinforcement learning\.External Links:2507\.08649,[Link](https://arxiv.org/abs/2507.08649)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, W\. Li, J\. Liu, M\. Jamnik, T\. Lacroix, Y\. Wu, and G\. Lample \(2023\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.External Links:2210\.12283,[Link](https://arxiv.org/abs/2210.12283)Cited by:[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1)\.
- C\. Kaliszyk, J\. Urban, H\. Michalewski, and M\. Olšák \(2018\)Reinforcement learning of theorem proving\.External Links:1805\.07563,[Link](https://arxiv.org/abs/1805.07563)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- G\. Lample, M\. Lachaux, T\. Lavril, X\. Martinet, A\. Hayat, G\. Ebner, A\. Rodriguez, and T\. Lacroix \(2022\)HyperTree proof search for neural theorem proving\.External Links:2205\.11491,[Link](https://arxiv.org/abs/2205.11491)Cited by:[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1)\.
- Y\. Li, D\. Du, L\. Song, C\. Li, W\. Wang, T\. Yang, and H\. Mi \(2025a\)HunyuanProver: a scalable data synthesis framework and guided tree search for automated theorem proving\.External Links:2412\.20735,[Link](https://arxiv.org/abs/2412.20735)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p4.1),[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1)\.
- Y\. Li, M\. Liu, R\. Wang, W\. Ji, Z\. He, R\. Pan, J\. Huang, T\. Zhang, and Y\. R\. Fung \(2025b\)Lean4Physics: comprehensive reasoning framework for college\-level physics in lean4\.External Links:2510\.26094,[Link](https://arxiv.org/abs/2510.26094)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p5.1),[Results](https://arxiv.org/html/2608.28639#Sx5.p1.1),[Physlib library](https://arxiv.org/html/2608.28639#Sx7.SSx3.SSS0.Px2.p1.1),[Datasets](https://arxiv.org/html/2608.28639#Sx8.p4.1)\.
- H\. Lin, Z\. Sun, S\. Welleck, and Y\. Yang \(2025a\)Lean\-star: learning to interleave thinking and proving\.External Links:2407\.10040,[Link](https://arxiv.org/abs/2407.10040)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- Y\. Lin, S\. Tang, B\. Lyu, J\. Wu, H\. Lin, K\. Yang, J\. Li, M\. Xia, D\. Chen, S\. Arora, and C\. Jin \(2025b\)Goedel\-prover: a frontier model for open\-source automated theorem proving\.External Links:2502\.07640,[Link](https://arxiv.org/abs/2502.07640)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun, J\. Wu, J\. Gesi, X\. Lu, D\. Acuna, K\. Yang, H\. Lin, Y\. Choi, D\. Chen, S\. Arora, and C\. Jin \(2025c\)Goedel\-prover\-v2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.External Links:2508\.03613,[Link](https://arxiv.org/abs/2508.03613)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p1.1),[Introduction](https://arxiv.org/html/2608.28639#Sx1.p5.1),[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1),[Results](https://arxiv.org/html/2608.28639#Sx5.p1.1)\.
- T\. Nipkow, L\. C\. Paulson, and M\. Wenzel \(2002\)Isabelle/hol: a proof assistant for higher\-order logic\.Lecture Notes in Computer Science, Vol\.2283,Springer\-Verlag\.Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p1.1)\.
- A\. Poiroux, V\. Kuncak, and A\. Bosselut \(2025\)LeanInteract: a python interface for lean 4External Links:[Link](https://github.com/augustepoiroux/LeanInteract)Cited by:[Lean 4 Proof Evaluation Infrastructure](https://arxiv.org/html/2608.28639#Sx2.SSx6.p3.1)\.
- S\. Polu, J\. M\. Han, K\. Zheng, M\. Baksys, I\. Babuschkin, and I\. Sutskever \(2022\)Formal mathematics statement curriculum learning\.External Links:2202\.01344,[Link](https://arxiv.org/abs/2202.01344)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- S\. Polu and I\. Sutskever \(2020\)Generative language modeling for automated theorem proving\.External Links:2009\.03393,[Link](https://arxiv.org/abs/2009.03393)Cited by:[Formal Theorem Proving with Large Language Models](https://arxiv.org/html/2608.28639#Sx2.SSx1.p1.1)\.
- Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. Ruan \(2025\)DeepSeek\-prover\-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.External Links:2504\.21801,[Link](https://arxiv.org/abs/2504.21801)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p1.1),[Introduction](https://arxiv.org/html/2608.28639#Sx1.p5.1),[Introduction](https://arxiv.org/html/2608.28639#Sx1.p6.1),[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1),[Reward Hacking in Reinforcement Learning](https://arxiv.org/html/2608.28639#Sx2.SSx5.p1.1),[Results](https://arxiv.org/html/2608.28639#Sx5.p1.1),[Reward Hacking Analysis\.](https://arxiv.org/html/2608.28639#Sx6.SSx3.SSS0.Px1.p1.4),[Potential Exploit Identification\.](https://arxiv.org/html/2608.28639#Sx6.SSx3.SSS0.Px2.p1.1),[Potential Exploit Identification\.](https://arxiv.org/html/2608.28639#Sx6.SSx3.SSS0.Px2.p2.1),[Potential Exploit Identification\.](https://arxiv.org/html/2608.28639#Sx6.SSx3.SSS0.Px2.p4.1),[Reproduction protocol and comparability to published results](https://arxiv.org/html/2608.28639#Sx7.SSx3.SSS0.Px1.p2.1),[Example: A Potential Compiler Exploit](https://arxiv.org/html/2608.28639#Sx7.SSx3.p2.5)\.
- M\. D\. Santos, H\. Wang, H\. de Saxcé, R\. Wang, M\. Baksys, M\. Unsal, J\. Liu, Z\. Liu, and J\. Li \(2025\)Kimina lean server: technical report\.External Links:2504\.21230,[Link](https://arxiv.org/abs/2504.21230)Cited by:[Lean 4 Proof Evaluation Infrastructure](https://arxiv.org/html/2608.28639#Sx2.SSx6.p4.1),[Server rewardrs∈\[0,1\]r\_\{s\}\\in\[0,1\]\.](https://arxiv.org/html/2608.28639#Sx4.SSx3.SSS0.Px2.p1.5)\.
- A\. Thakur, G\. Tsoukalas, Y\. Wen, J\. Xin, and S\. Chaudhuri \(2024\)An in\-context learning agent for formal theorem\-proving\.External Links:2310\.04353,[Link](https://arxiv.org/abs/2310.04353)Cited by:[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1)\.
- G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. Chaudhuri \(2024\)PutnamBench: evaluating neural theorem\-provers on the putnam mathematical competition\.External Links:2407\.11214,[Link](https://arxiv.org/abs/2407.11214)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p5.1),[Results](https://arxiv.org/html/2608.28639#Sx5.p1.1),[Datasets](https://arxiv.org/html/2608.28639#Sx8.p3.1)\.
- H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. D\. Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu, J\. Lu, H\. de Saxcé, B\. Bailey, C\. Song, C\. Xiao, D\. Zhang, E\. Zhang, F\. Pu, H\. Zhu, J\. Liu, J\. Bayer, J\. Michel, L\. Yu, L\. Dreyfus\-Schmidt, L\. Tunstall, L\. Pagani, M\. Machado, P\. Bourigault, R\. Wang, S\. Polu, T\. Barroyer, W\. Li, Y\. Niu, Y\. Fleureau, Y\. Hu, Z\. Yu, Z\. Wang, Z\. Yang, Z\. Liu, and J\. Li \(2025\)Kimina\-prover preview: towards large formal reasoning models with reinforcement learning\.External Links:2504\.11354,[Link](https://arxiv.org/abs/2504.11354)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p1.1),[Introduction](https://arxiv.org/html/2608.28639#Sx1.p5.1),[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1),[Results](https://arxiv.org/html/2608.28639#Sx5.p1.1)\.
- X\. Wang, M\. Tian, Y\. Zeng, Z\. Huang, J\. Yuan, B\. Chen, J\. Xu, M\. Zhou, W\. Liu, M\. Wu, Z\. Guo, Q\. Qian, Y\. Wang, F\. Zhang, R\. Yin, S\. Dou, C\. Lv, T\. Chen, K\. Song, X\. Tan, T\. Gui, X\. Zheng, and X\. Huang \(2026\)Reward hacking in the era of large models: mechanisms, emergent misalignment, challenges\.External Links:2604\.13602,[Link](https://arxiv.org/abs/2604.13602)Cited by:[Reward Hacking in Reinforcement Learning](https://arxiv.org/html/2608.28639#Sx2.SSx5.p1.1)\.
- M\. Wu, M\. Norrish, C\. Walder, and A\. Dezfouli \(2021\)TacticZero: learning to prove theorems from scratch with deep reinforcement learning\.External Links:2102\.09756,[Link](https://arxiv.org/abs/2102.09756)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- Z\. Wu, S\. Huang, Z\. Zhou, H\. Ying, Z\. Yuan, W\. Zhang, D\. Lin, and K\. Chen \(2025\)InternLM2\.5\-stepprover: advancing automated theorem proving via critic\-guided search\.External Links:2410\.15700,[Link](https://arxiv.org/abs/2410.15700)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- H\. Xin, Z\. Z\. Ren, J\. Song, Z\. Shao, W\. Zhao, H\. Wang, B\. Liu, L\. Zhang, X\. Lu, Q\. Du, W\. Gao, Q\. Zhu, D\. Yang, Z\. Gou, Z\. F\. Wu, F\. Luo, and C\. Ruan \(2024\)DeepSeek\-prover\-v1\.5: harnessing proof assistant feedback for reinforcement learning and monte\-carlo tree search\.External Links:2408\.08152,[Link](https://arxiv.org/abs/2408.08152)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- R\. Xin, C\. Xi, J\. Yang, F\. Chen, H\. Wu, X\. Xiao, Y\. Sun, S\. Zheng, and K\. Shen \(2025\)BFS\-prover: scalable best\-first tree search for llm\-based automatic theorem proving\.External Links:2502\.03438,[Link](https://arxiv.org/abs/2502.03438)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p4.1),[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1)\.
- K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar \(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.External Links:2306\.15626,[Link](https://arxiv.org/abs/2306.15626)Cited by:[Formal Theorem Proving with Large Language Models](https://arxiv.org/html/2608.28639#Sx2.SSx1.p1.1),[Tree Search for Theorem Proving](https://arxiv.org/html/2608.28639#Sx2.SSx2.p1.1),[Lean 4 Proof Evaluation Infrastructure](https://arxiv.org/html/2608.28639#Sx2.SSx6.p2.1)\.
- S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. L\. Griffiths, Y\. Cao, and K\. Narasimhan \(2023\)Tree of thoughts: deliberate problem solving with large language models\.External Links:2305\.10601,[Link](https://arxiv.org/abs/2305.10601)Cited by:[Monte Carlo Tree Search in Language Model Reasoning](https://arxiv.org/html/2608.28639#Sx2.SSx3.p1.1)\.
- H\. Zhang, R\. Wang, R\. Pan, W\. Wang, B\. Meng, and T\. Zhang \(2026\)PhysProver: advancing automatic theorem proving for physics\.External Links:2601\.15737,[Link](https://arxiv.org/abs/2601.15737)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p5.1),[Results](https://arxiv.org/html/2608.28639#Sx5.p1.1),[Datasets](https://arxiv.org/html/2608.28639#Sx8.p5.1)\.
- J\. Zhang, Q\. Wang, X\. Ji, Y\. Liu, Y\. Yue, F\. Zhang, D\. Zhang, G\. Zhou, and K\. Gai \(2025\)Leanabell\-prover: posttraining scaling in formal reasoning\.External Links:2504\.06122,[Link](https://arxiv.org/abs/2504.06122)Cited by:[Whole\-Proof Generation](https://arxiv.org/html/2608.28639#Sx2.SSx4.p1.1)\.
- K\. Zheng, J\. M\. Han, and S\. Polu \(2022\)MiniF2F: a cross\-system benchmark for formal olympiad\-level mathematics\.External Links:2109\.00110,[Link](https://arxiv.org/abs/2109.00110)Cited by:[Introduction](https://arxiv.org/html/2608.28639#Sx1.p5.1),[Results](https://arxiv.org/html/2608.28639#Sx5.p1.1),[Datasets](https://arxiv.org/html/2608.28639#Sx8.p2.1)\.