Paper deep dive
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
Matěj Kripner, Milan Straka
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 10/10/2026, 2:01:44 AM
Summary
The paper introduces NanoProof, the first open, end-to-end reproducible factorized execution-guided automated theorem prover for Lean 4. It releases the training data (LeanTree dataset), extraction tooling, training pipeline, and model weights. NanoProof achieves 50.8% pass@16 on MiniF2F-Test, outperforming similar systems like HyperTree Proof Search and ABEL while using significantly less compute (90x and 7x less, respectively, and four orders of magnitude less than AlphaProof). The system leverages a structured proof tree dataset, reinforcement learning with a self-improvement loop, and specific search techniques like proof simplification, cycle detection, and diverse tactic sampling.
Entities (11)
Relation Signals (8)
NanoProof → achievesscoreon → MiniF2F-Test
confidence 100% · NanoProof achieves 50.8% pass@16 on MiniF2F-Test
Matěj Kripner → affiliatedwith → Charles University Prague
confidence 100% · Matěj Kripner... Institute of Formal and Applied Linguistics... Charles University Prague
Milan Straka → affiliatedwith → Charles University Prague
confidence 100% · Milan Straka... Institute of Formal and Applied Linguistics... Charles University Prague
NanoProof → uses → Lean 4
confidence 100% · NanoProof... theorem prover in Lean 4
LeanTree → extractedfrom → Mathlib
confidence 95% · dataset of 92,927 independently verified structured proof trees extracted from Mathlib
NanoProof → outperforms → ABEL
confidence 90% · exceeding the two closest systems of its class... ABEL... at... 7x less compute
NanoProof → outperforms → HyperTree Proof Search
confidence 90% · exceeding the two closest systems of its class, HyperTree Proof Search... at roughly 90x... less compute
NanoProof → useslesscomputethan → AlphaProof
confidence 90% · using more than four orders of magnitude less compute than AlphaProof
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources. To this end, we build and release a dataset of structured proof trees, as well as a tool for programmatic interaction and data extraction within the Lean 4 formal verifier. To support sustainable research, we focus on compute efficiency to facilitate accessible training and evaluation. NanoProof achieves 50.8% pass@16 on MiniF2F-Test, exceeding the two closest systems of its class, HyperTree Proof Search and ABEL, at roughly 90x and 7x less compute, and using more than four orders of magnitude less compute than AlphaProof. Stronger open-weight provers exist, but they are fine-tuned from large pretrained language models and release neither training data nor pipeline; NanoProof shows that the factorized execution-guided class of provers can be rebuilt from scratch with modest resources.
Tags
Links
- Source: https://arxiv.org/abs/2610.11605v1
- Canonical: https://arxiv.org/abs/2610.11605v1
Trouble viewing inline? Open PDF directly →
Full Text
73,760 characters extracted from source content.
Expand or collapse full text
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 Matěj Kripner ∗ Milan Straka Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University Prague, Czech Republic Abstract We introduce NanoProof, to our knowledge the first factor- ized execution-guided theorem prover in Lean 4 whose train- ing data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources. To this end, we build and release a dataset of structured proof trees, as well as a tool for pro- grammatic interaction and data extraction within the Lean 4 formal verifier. To support sustainable research, we focus on compute efficiency to facilitate accessible training and eval- uation. NanoProof achieves 50.8% pass@16 on MiniF2F-Test, exceeding the two closest systems of its class, HyperTree Proof Search and ABEL, at roughly 90×and 7×less compute, and using more than four orders of magnitude less compute than AlphaProof. Stronger open-weight provers exist, but they are fine-tuned from large pretrained language models and release neither training data nor pipeline; NanoProof shows that the factorized execution-guided class of provers can be rebuilt from scratch with modest resources. 1 Introduction In automated theorem proving (ATP), the task at hand con- sists of generating a valid proof to a mathematical statement. We focus our attention on formal ATP, where both the state- ment and the proof are expressed in a formal language such as Lean 4 [29]. In this setting, the correctness of a generated proof can be verified automatically, providing clear feedback to an ATP system, which can be used for training using reinforcement learning (RL). Formal methods have found applications in the formal- ization of mathematics [36], physics [34], and chemistry [3], as well as software verification [2], cryptography [8], and general reasoning [16]. With the current and anticipated rise of AI-generated code, proofs, and other artifacts, we expect human verification to become the bottleneck to in- novation, making formal methods essential for their ability to automatically filter out incorrect solutions. For example, mathematicians already benefit from expediting the review process in frontier research by submitting a formalization of their results [12]. Similarly, formal verification enables massively collaborative mathematical projects without the need for extensive human moderation [4]. ∗ Corresponding author: kripner@ufal.mff.cuni.cz. On an implementation level, ATP systems can be divided along several axes. First, in an execution-guided proof search, a prover interleaves proof search with verification, leverag- ing feedback from the formal verifier after each proof step and generating steps conditioned on the true internal proof state. For example, in Lean 4, an execution-guided prover ob- serves the list of currently open goals and is informed on any proof steps that resulted in an error. In contrast, execution- agnostic provers only use the formal verifier to verify the final proof, generating proof steps with no feedback about the validity of preceding steps or the current internal proof state. Thus, in execution-agnostic search, it falls upon the proof step generator to deduce the evolving proof state, as this is a necessary precondition to determine the validity of subsequent proof steps. This coupling of a policy model and a world model increases the complexity of proof generation. Second, in a factorized proof search, the prover is allowed to split proof states into separate branches that can be ex- plored independently. An illustrative example is mathemat- ical induction, where factorized search considers the base case and the inductive case independently, enabling paral- lelization and dynamic allocation of search budget between the two branches. The utility of node re-use and paralleliza- tion enabled by factorization has been verified by Lample et al. [22]and Hubert et al. [14]and we do not reiterate it in this work. In contrast, in a linear proof search, the proof state consists of all the context necessary to complete the proof. Finally, in an any-time proof search, the prover perfor- mance grows when time or compute budget is increased, while a one-shot prover can only be scaled by running multi- ple instances in parallel, without the possibility of utilizing results across searches. Proof search can be treated as a generic text-to-text language modeling problem of generating a proof given a statement, resulting in a linear one-shot execution-agnostic method. Such methods have directly benefited from the recent rapid rise in capabilities of large language models (LLMs). In contrast, factorized any-time execution-guided provers require careful pre-processing of training data and tight integration with the verification framework. The existing systems of this class, HyperTree Proof Search [22], ABEL [11], and AlphaProof [14], released neither their data nor runnable code. Open execution-guided provers such as InternLM2.5-StepProver [40], BFS-Prover [43], and 1 arXiv:2610.11605v1 [cs.LG] 8 Oct 2026 Matěj Kripner and Milan Straka BFS-Prover-V2 [44] perform linear best-first search over monolithic proof states and release at most model weights. The factorized class has therefore been out of reach for the open-source community, both in terms of data availability and compute requirements. We identify this as a major roadblock to advancing Machine Learning-based ATP in the age of large models, particularly since recent approaches like AlphaProof [14] and HyperTree Proof Search [22] demonstrated the viability of this paradigm. Since the inception of this work, text-to-text and agen- tic provers built on large language models have become extremely strong, with Seed-Prover [5] and Goedel-Prover- V2 [25] saturating MiniF2F. We do not take this as evidence that search-based approaches are obsolete. Casting proving as plain text generation means that a frontier LLM can be applied without adaptation, whereas factorized search-based provers require structured training data, verifier integra- tion, and search infrastructure before they can run at all, and until now this machinery existed only inside closed sys- tems. Whether classical search with small models remains competitive with large generic LLMs at equal compute is an open question, and it can only be studied if this class of system exists in an open and reproducible form. More- over, the strongest approach may turn out to be a combi- nation of the two, LLM reasoning with verifier-grounded search, a direction that the heavy use of Lean feedback in Seed-Prover already explores. Factorized search also offers concrete advantages independent of model size: node re-use across branches, independent allocation of search budget to subgoals, and distance-to-proof-end labels that directly su- pervise the critic. This is why we consider open, reproducible tooling for the search-based side worth building. In this work, we address this reproducibility barrier by introducing NanoProof, an end-to-end ATP system that lever- ages existing open resources and provides the novel compo- nents necessary to complete the Lean 4 pipeline. Specifically, our contributions are as follows. •Data, Tooling, and Environment We release LeanTree, a dataset of 92,927 independently verified structured proof trees extracted from Mathlib, the extraction tool that produces such trees from any Lean 4 project, and a Lean interface with incremental kernel verification and a distributed environment pool for reinforcement learning. • ATP System We introduce a factorized any-time execution-guided prover called NanoProof and release all the tooling necessary to reproduce it and build on top of it. 1 • Performance Evaluation We demonstrate the ef- ficacy of NanoProof through an end-to-end training 1 The Python package and its source code is available at https://github.com /kripner/nanoproof. run, achieving 50.8% pass@16 on MiniF2F-Test [50] us- ing more than four orders of magnitude less compute than AlphaProof. • Search-Level Techniques We describe practical train-time and inference-time techniques, namely proof simplification and augmentation, cycle detec- tion, and diverse tactic sampling, and quantify their effect where our compute budget allowed. In Section 3, we present the training pipeline and the search algorithm of NanoProof. In Section 4, we describe the algorithm for extracting proof trees from human-authored Lean projects and the resulting LeanTree dataset, a necessary component for pre-training a factorized execution-guided prover. Finally, in Section 5, we present a training run of NanoProof using openly available datasets and LeanTree. The necessary background in Lean and proof search is avail- able in Appendix A. 2 Related Work We give a brief overview of Lean, different ATP approaches, and existing formal ATP datasets and benchmarks. Lean 4 [29] is a leading formal language for theorem proving with applications both in the formalization of math- ematics [36] and in numerous other domains [3,8,16,34]. One of the appealing properties of Lean is its extensibility, stemming from the fact that its theorem proving component is written in Lean itself, and the user can modify both its syn- tax and its semantics, which we heavily utilize in LeanTree. Execution-Agnostic ATP. ATP can be formulated as a text-to-text task so that any existing LLM is directly appli- cable. This approach to theorem proving was pioneered by Baldur [10]. More recently, LLMs using chain-of-thought refined using RL were utilized by DeepSeek-Prover-V2 [32], Kimina-Prover [38], InternLM-Math [49], Goedel-Prover- V2 [25], and Seed-Prover [5], among others, securing top positions on relevant benchmarks; Goedel-Prover-V2 reports 88.1% on MiniF2F-Test at pass@32 and Seed-Prover 99.6%. Execution-Guided ATP. In execution-guided ATP, a prover interacts with the verification system iteratively dur- ing the proof search, generating proof steps conditioned on the internal proof state. In neural theorem proving, this ap- proach was pioneered by Holophrasm [39] in Metamath [27], using a UCT-based [19] AND-OR tree search with a RNN sequence-to-sequence model for tactic enumeration and payoff prediction. Later extensions include GPT-f [30] and Evariste [22], the latter also targeting Lean 3 in addition to Metamath. ABEL [11] extended Evariste with incremental improvements and Lean 4 compatibility, but did not release the code or dataset. AlphaProof [14] then achieved a signifi- cant improvement in performance, unfortunately also with closed code and data. A separate line of open execution-guided provers performs linear best-first search over monolithic Lean proof states 2 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 Nemotron-C-Math-4+ 10B tokens LEAN-Github (raw) 64M tokens Mathlib 103k tactic proofs LeanTree 287k proof edges Fine-TuningMid-TrainingBase Training NuminaMath-LEAN 97k formal statements RL Loop Replay Buffer NanoProof Figure 1. NanoProof training pipeline. After supervised pretraining, the prover enters into a self-improvement loop where successfully discovered proofs are used for further training. Mid-training is not included in the final run, as described in Section 5. with a policy fine-tuned from a pretrained LLM: InternLM2.5- StepProver [40], BFS-Prover [43] with 72.95% on MiniF2F- Test, BFS-Prover-V2 [44] with 82.4% and 86.1% for its 7B and 32B models (95.1% with an additional Gemini 2.5 Pro planner), and MPS-Prover [23] with 75.82%. In the terminol- ogy introduced above, these are execution-guided but linear provers: none of them factorizes proof states into indepen- dently searchable goals with node re-use and metavariable- coupling handling. They release at most weights and infer- ence code, and none releases training data or pipeline. Being fine-tuned from Qwen2.5 [46], their reported budgets ex- clude the pre-training of the base model, on the order of 10 12 TFLOPs, and their undisclosed pre-training corpora cannot be audited for benchmark contamination. BFS-Prover also argues that, in its setting of a large pretrained policy and no learned critic, simple best-first search can outperform MCTS- style search; whether this carries over to factorized search with a trained critic is an open question that our release makes testable. Datasets. The standard library of Lean, Mathlib [7], offers more than 124k formal definitions and 255k formal proofs. Together with numerous formalization projects created by the community, this offers a sizable human-written dataset for the supervised training of theorem provers. However, execution-guided ATP approaches require addi- tional data pre-processing to expose the intermediate proof states. Such a dataset was first provided by LeanStep [13] in Lean 3 by extracting tactic invocation data from Mathlib. LeanDojo [47] extends this approach to Lean 4, additionally providing information about the premises used in each tactic application, necessary for training retrieval-augmented ap- proaches. Similar datasets are also offered by Pantograph [1] and lean-training-data [28]. However, none of these datasets offers tactic proofs in a structured, simplified format, which is needed for NanoProof training. Most importantly, they do not contain distance-to-proof-end information. Additionally, Lean-Workbook [48], DeepSeek-Prover- V1 [42], and NuminaMath-LEAN [38] provide large collec- tions of automatically formalized proofs of various quality, the latter also offering a sizable human-formalized portion. Benchmarks. MiniF2F [50] offers 488 problems drawn from mathematical olympiad and undergraduate mathemat- ics courses, formalized in parallel in Lean 3, Metamath, Is- abelle, and HOL Light. The objective is to generate valid formal proofs of the statements. The benchmark was later ported to Lean 4 by Yang et al. [47], with some formaliza- tion errors corrected by Wu et al. [40]. We use MiniF2F as released by Hubert et al. [14]. 3 NanoProof Automated Theorem Prover We describe the training and inference mechanism of NanoProof. Section 3.1 mostly follows Hubert et al. [14], while the following sections describe our implementation choices and additions; the LeanTree dataset and extraction tool that enable the supervised training of such a prover are described in Section 4. 3.1 Proof Search Algorithm RL Environment. We formulate the proof search process as an RL environment. At episode start, a formal theorem statement is sampled from a corpus (cf. Section 5). At each step, the prover (agent) observes the current state푠 푡 consist- ing of the list of open goals yet to be proven, and generates an action푎 푡 , i.e., a Lean tactic. The Lean verifier then imple- ments the transition function from the pair(푠 푡 ,푎 푡 )to the list of next states(푠 1 푡+1 , . . .,푠 푛 푡+1 ), potentially empty. Note that this deviates from a simple Markov Decision Process in that the agent proceeds independently into each next state. Recall that for the goals in state푠 푡 to be proven, it is necessary to prove all goals in states(푠 1 푡+1 , . . .,푠 푛 푡+1 ). 3 Matěj Kripner and Milan Straka The episode ends when a valid action has been assigned to each state, yielding a proof tree. The agent is then as- signed a reward푟=−푑, where푑is the depth of the proof tree. This incentivizes the agent to find short proofs that maximize branching, utilizing the factorization capability outlined above. MCTS Search. Our proof search algorithm follows closely that of AlphaProof, and we leave detailed description to Hu- bert et al. [14]. The prover consists of an actor predicting which proof tactic to apply in the current proof state, and a critic predicting future reward in the current proof branch, i.e., the negative depth of the proof sub-tree starting from the current state. The algorithm maintains an AND-OR search tree that initially contains only the root node with the theo- rem to be proven and is then iteratively expanded by repeat- ing three phases: selection, expansion and backpropagation, adapted from AlphaZero [33] and Sampled MuZero [15]. At node expansion, generated tactics are immediately executed in Lean, and invalid ones are discarded. Compared to sequen- tial two-player games, the prover agent does not commit to intermediate actions and only performs a single search for each theorem. For this reason, Hubert et al. [14]incorporates a progressive sampling mechanism, allowing new tactics to be sampled for internal nodes. Matchmaker. Theorems to be proven are sampled from a corpus with sampling weights determined by a simple heuristic matchmaker. After initialtrust_countattempts at each theorem, the matchmaker down-weights theorems that have been proven at leasttrust_count_provedin a row and theorems that have never been proved, thus prioritizing theorems at the edge of the prover’s current ability. Com- pared to Hubert et al. [14], we additionally down-weight theorems for which a single-tactic proof has been found, since no shorter proof can be discovered. 3.2 Network Architecture The actor and critic are modeled using a single Transformer model [37] based on nanochat [17]. 2 Instead of utilizing ded- icated actor and critic heads, we adopt the simpler approach of shared vocabulary by Polu and Sutskever[30]. Specifi- cally, the model input consists of a tokenized pretty-printed Lean state followed by a special token indicating whether what follows is a tactic or a critic value. During inference, tactics are decoded autoregressively. In contrast, prediction of the critic value is done with only a single forward pass and weighted averaging of the value bins based on predicted token probabilities. For tokenization, we use the GPT-2 tokenizer [31] 3 ex- tended with dedicated tokens for symbols that occur at least 1,000×in Mathlib. The range of allowed critic values is di- vided into discrete bins using dedicated tokens [9]. 2 https://github.com/karpathy/nanochat, MIT License 3 https://huggingface.co/openai-community/gpt2, MIT License 3.3 Training Pipeline As shown in Figure 1, the prover network undergoes several supervised training phases before entering a self- improvement loop. This preliminary phase is necessary because the generation of valid and diverse tactics is a challenging task in itself. The supervised phases use in- creasingly targeted training data, starting with general math-related text and progressing through Lean source code to highly pre-processed human-authored Lean proofs. This progression of data quality is mirrored in an increasingly limited quantity. During the self-improvement loop, the prover continu- ously samples theorems from an autoformalized corpus and attempts to prove them, storing all successful proofs in a replay buffer. Transitions sampled from the replay buffer are then used as further training data for the prover network. In addition, a given fraction of supervised fine-tuning data is mixed in with the collected data to increase training stability. The system alternates between collecting푛 samples new proof transitions and performing 푛 updates gradient updates. As shown in Figure 2, the RL loop infrastructure features an inference server with simple first-available load balancing, a distributed trainer and detached Lean servers running on CPU nodes. 3.4 Lean Integration LeanTree offers a Python interface built on top of Lean REPL [6]. After initiating a proof search and applying a Lean tactic to a given proof state, LeanTree returns a list of resulting sub-states. The interface is suitable for tree search and backtracking as the interaction can be restarted from any intermediate proof state. Additionally, given the high CPU requirements of Lean 4, LeanTree implements a dy- namic pool of environments exposed over HTTP endpoint for deployment to CPU nodes during distributed training. During our work, we encountered invalid proofs that Lean REPL accepted as valid; the details and a correction are described in Appendix E. Note that all proofs found by NanoProof are independently verified by exporting them as standalone Lean code. 3.5 Proof Simplification and Augmentation Proof Simplification. We attempt to simplify the proofs produced by the proof search algorithm by pruning redun- dant tactics. This is done both during experience collection to improve the quality of the data saved to the replay buffer and during final inference to enhance the readability of the generated proofs for humans. In a representative RL run, our algorithm was able to simplify 59% of proofs longer than one tactic. An example of a simplified proof recorded during an experience collection phase is shown in Appendix C. The proof simplification algorithm is outlined in Listing 1. Given a generated proof, the simplification aims to extract 4 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 a minimal sub-proof that still proves the original theorem. Starting with a proof tree, we consider each non-leaf edge individually. If contracting an edge leaves the proof valid, the edge is removed. For a non-leaf edge푒=(푠 푡 ,푠 푡+1 )with tactic 푎 푡 , contraction is implemented by discarding푎 푡 (together with 푠 푡+1 ), replacing it with any tactic 푎 푡+1 applied in 푠 푡+1 . When re-verifying the proof after contraction, it suffices to verify the modified proof sub-tree below푠 푡 , since other branches and tactics on the path to root are not affected. The sub-tree is verified by re-executing each tactic application in it, starting with the application of푎 푡+1 . When푎 푡 produces multiple factorized goals, i.e., it has more than one child node, we individually attempt to execute each of the sub-trees, and 푒is deemed redundant when at least one execution succeeds. After a node is removed, the whole simplification process is restarted because removing an edge might only be possible after a different edge is removed first. Proof Augmentation. When sampling a proof from the replay buffer, we apply a random augmentation to each of its proof edges, altering them while preserving their semantics. First, all hypotheses and goals are randomly renamed with probability푝 rename , applying the rename accordingly also in both the tactic and the other hypotheses. Second, the hy- potheses in each goal are randomly shuffled with probability 푝 shuffle . 3.6 Cycle Detection We apply a cycle detection mechanism during node expan- sion. When a tactic application results in a goal퐺that is equivalent to a goal퐺 ′ already present on the path to root, the tactic is discarded. Any final proof containing this tactic could equivalently be found by solving퐺directly instead of descending to퐺 ′ . In a representative run, 18% of otherwise valid tactics were rejected due to cycle detection. Note that goal equivalence is checked at the syntactic level up to goal re-shuffling, goal renaming, and whitespace changes. 3.7 Diverse Tactic Sampling We observe that the autoregressive tactic sampling often produces duplicate tactics, sometimes constraining node ex- pansion to just a single action, particularly in the case of short one-token tactics. In a representative run, 32% of nodes had their action count reduced due to duplicated sampling. We address this by forcing diverse sampling on the first tactic token. Specifically, the first sampling step employs the Gumbel-Top-푘trick [20] to cap each possible token to first_token_capoccurrences. Taking an average over last three saved checkpoints in the same run, this diverse tac- tic sampling increased performance on MiniF2F-Valid by 2.0 percentage points under 16 simulations, highlighting its importance for small compute budgets. 4 Structured Proof Tree Dataset To enable supervised pretraining on existing human-written Lean proofs, factorized execution-guided provers require careful pre-processing of proofs into structured proof trees. The challenge is twofold: First, the Lean language under- stands a proof as a linear sequence of tactics, instead of a tree where different branches can be produced independently. These tactics can be nested and combined with tactic combi- nators as well as other syntactic sugar. Second, Lean proofs, as present in human-written repositories, are written in a compact, refined way to make them easy to read, maintain, and build on. However, we seek a different proof style, one that unfolds the proof in a way amenable to search, i.e., in small incremental steps. To address this challenge, we introduce a proof extrac- tion tool and dataset, collectively calledLeanTree, whose preliminary version was presented in Kripner et al. [21]. In each extracted proof tree, a node carries a single goal, 4 and an edge corresponds to a tactic application operating on that goal. The dataset contains 92,927 extracted proof trees from a recent version of Mathlib, 5 the standard library of human-written proofs in Lean. Details about the structure of the dataset are provided in Appendix H. Importantly, each included tree is independently verified by executing it from the root down in topological order. Because of technical challenges outlined in this section, not all tactic proofs can currently be verifiably converted. Specifically, 9.53% of tactic proofs in Mathlib were not included in LeanTree because the validity of all tactics in the extracted proof trees could not be verified. We are continually working on perfecting this process. The LeanTree dataset, together with its documentation and relevant metadata, is publicly available at https://hugg ingface.co/datasets/ufal/leantree. The extraction tool and the Lean interface are available at https://github.com/kripn er/leantree. Proof Tree Building. To illustrate the challenges in build- ing a proof tree, Figure 3 shows two example Lean proofs and the resulting trees. For the purposes of illustration, we do not utilize powerful tactics such aslinarith, which would solve the trivial theorem nearly automatically. Instead, we show- case branching, metavariable coupling, and the introduction of a new hypothesis. Other Lean features not shown in Figure 3 that further complicate the construction of proof trees include tactic combinators such astry,iterate, andany_goals, where the set of affected goals is determined in runtime, constructs such asall_goalsand<;>that go against tree formulation due to operating on multiple goals, or tactics such asswitch and rotate_left that change the order of open goals. 4 Note that, due to metavariable coupling, nodes occasionally contain more than one goal, which we detail in Section 4.3. 5 leanprover/lean4:v4.27.0, Apache-2.0 License 5 Matěj Kripner and Milan Straka Algorithm 1 Pruning of redundant tactics. Input: proof tree 푃 procedure PruneTactics(푃) for any non-leaf 푒=(푠 푡 ,푠 푡+1 ) with action 푎 푡 for any 푎 푡+1 applied in 푠 푡+1 푃 ′ ← contract(푃,푒,푎 푡 ← 푎 푡+1 ) if subtree_valid(푠 푡 ,푃 ′ ) return PruneTactics(푃 ′ ) end if end for end for return 푃 RL Trainer Lean Ser ver Process Pool Inference Router DDP Trainer Replay Buffer Prover Server ... Coordinator Lean Ser ver Process Pool Figure 2. Runtime architecture of RL training. We implement the proof extraction in three stages de- scribed in the following three subsections. A comparison of LeanTree with existing datasets and tools for training data extraction in Lean is given in Appendix G. 4.1 Singleton Tree Construction The first stage of proof tree building transforms a Lean proof into a singleton tree, where each node contains a single goal, by matching tactic applications with the goals they affect. In general, a tactic application transforms a list of open goals into an entirely new list of open goals without any addi- tional guarantees, making this transformation nontrivial. To build singleton trees, we integrate Lean REPL with an augmented version of the BetterParser module of Paper- Proof [18], 6 which solves an analogous problem, although originally developed for visualization purposes. 4.2 Tactic Simplification Singleton trees are modified so that complex tactics are bro- ken down into simpler ones, and each tactic is a valid self- contained proof step. We now describe some of these modi- fications. Nested Tactics. Tactics parametrized by a term can them- selves contain nested tactic blocks. For example, consider the following tactic from the Complex Analysis module in Mathlib. exact ⟨by rw [aeval_algHom_apply, hw, map_zero], rfl⟩ (1) 6 https://github.com/Paper-Proof/paperproof, MIT License In Listing 1, theexacttactic is parametrized by a term which contains a tactic block introduced using thebykey- word. We break down this complex proof step by masking the nested tactic block and instead spawning a child goal, yielding the following series of simpler proof steps. exact ⟨by sorry, rfl⟩ rw [aeval_algHom_apply] rw [hw] rw [map_zero] (2) Note that therfltactic is not masked since it is used as a term instead of a tactic. calcBlocks. Thecalctactic combines a sequence of relational proofs into a single transitive derivation. We de- compose such a block into onehavetactic per step, followed by a finalexacttactic that combines the intermediate lem- mas. An example is shown in Figure 3. Structuring Tactics. Thecasesandinductiontactics introduce syntactic branching by partitioning a proof based on the value of an inductive type. The tactic optionally con- tains a solving branch for each of the constructors of such a type. We move the individual proof branches from thecases orinductiontactic into their separate proof steps. For ex- ample, consider thecasestactic in Figure 3, which spans 10 lines and should not be presented to a policy model as a training sample. MergedrwTactics. In Lean, subsequentrwtactics can be merged into a single tactic, which is commonplace in human-written proofs. We partition such composite tactics into individual rw tactics. 6 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 open Nat theorem succ_less_double_succ (n : Nat) : n > 0 → n < 2 * n := by intro h cases n with | zero => apply h | succ n' => apply le_trans case m => exact n' + 2 · rfl · rw [two_mul, add_succ] have h1 : 1 ≤ n' + 1 · apply succ_le_succ (zero_le _) · exact add_le_add_left h1 (n' + 1) import Mathlib.Algebra.Group.Basic import Mathlib.Algebra.Order.Monoid.Unbundled.Basic import Mathlib.Order.Lattice variable α : Type* variable [PartialOrder α] [AddCommSemigroup α] a b c d : α variable [AddLeftReflectLE α] theorem tsub_eq_tsub_of_add_eq_add (h : a + d = c + b) : a - b = c - d := by calc a - b = a + d - d - b := by rw [add_tsub_cancel_right] _ = c + b - b - d := by rw [h, tsub_right_comm] _ = c - d := by rw [add_tsub_cancel_right] h : a + d = c + b ⊢ a - b = c - d h h1 ⊢ a - b = c - d have h1 : a - b = a + d - d - b have h2 : a + d - d - b = c + b - b - d h h1 h2 ⊢ a - b = c - d · exact Trans.trans h1 (Trans.trans h2 h3) h ⊢ a - b = a + d - d - b rw [add_tsub_cancel_right] h h1 ⊢ a - b = a + d - d - b rw [h, tsub_right_comm] ⊢ n > 0 → n < 2 * n cases n h : 0 > 0 ⊢ 0 < 2 * 0 h : n✝ + 1 > 0 ⊢ n✝ + 1 < 2 * (n✝ + 1) case succ n' h : n' + 1 > 0 ⊢ n' + 1 < 2 * (n' + 1) apply Nat.le_trans h : n' + 1 > 0 ⊢ (n' + 1).succ ≤ ?m ⊢ ?m ≤ 2 * (n' + 1) ⊢ ℕ case m => exact n' + 2 h : n' + 1 > 0 ⊢ n' + 2 ≤ 2 * (n' + 1) rfl have h1 : 1 ≤ n' + 1 apply h · · · · Mathlib LeanTree Factorize proof states. Simplify nested tactics, structuring tactics, calc blocks, composite rw tactics, ... Merge metavariable-dependent goals. Figure 3. LeanTree extracts Lean proofs from a Lean file (top) and transforms them into structured proof trees (bottom). Synthetic tactics in the proof tree are marked using dashed border. 4.3 Merging Metavariable-Dependent Goals To obtain the final proof tree, sibling nodes in a singleton tree are merged if they share a metavariable. This corre- sponds to the fact that metavariable-dependent goals cannot be explored independently. During this merging process, the entire proof tree is ex- ecuted starting from the root state and following each tree edge, verifying that each proof branch ends in a proven state. In this way, we ensure the correctness of the whole proof tree building process. Proof trees that fail this verification are not included in the final dataset. In Figure 3, observe that applyingNat.le_transyields three goals that are not split due to a shared metavariable ?m. However, once the metavariable is assigned usingexact, the remaining two goals are now independent and can be split. 7 Matěj Kripner and Milan Straka 020406080100 Step 34 36 38 40 42 44 46 48 50 52 MiniF2F-Valid (%) 42.4% (n sim = 8) 47.0% (n sim = 32) 49.9% (n sim = 128) 51.3% (n sim = 256) Figure 4. Prover performance throughout RL training. We show how NanoProof success rate on MiniF2F scales with RL training time and number of simulations푛 sim . Averaged over three independent runs with min/max bands. 10 9 10 10 10 11 10 12 10 13 Compute (TFLOPs) 0 20 40 60 80 100 MiniF2F-Test (%) Closed-Source Factorized Any-Time Execution-Guided AlphaProof (TTRL) HTPS ABEL DeepSeek-Prover-V2 ReProver BFS-Prover NanoProof Figure 5. FLOPs vs performance comparison. We show ATP success rate on MiniF2F-Test relative to approximate total compute requirements. FLOPs are converted by us from reported hardware usage, or estimated where it is not dis- closed (Appendix F). 5 Experiments We present an end-to-end training run of NanoProof. The prover policy and critic network is first trained in a super- vised fashion before entering into a self-improvement loop as described in Section 3.3. We describe both of these phases be- low, with key hyperparameters listed in Appendix B. Hyper- parameters were chosen manually after several experiments on MiniF2F-Valid, leaving MiniF2F-Test for final evaluation. Supervised Training. First, we base train the network on the first 10B tokens of the Nemotron-C-Math-4+ dataset [26], 7 containing math and code related text. Then, we fine-tune the network on the 287k pre-processed proof steps from Mathlib [7] contained in LeanTree, leaving the last 10% of files (amounting to 29k proof steps) for validation and training on the remaining 258k. Each proof step con- sists of a proof state, tactic, and distance to proof end, i.e., the corresponding sub-proof depth. The data used during fine-tuning necessitate careful pre-processing described in Section 4. We additionally experimented with inserting a mid-train phase between base training and fine-tuning, consisting of additional training on 64M tokens of Lean code scraped from GitHub repositories listed in the LEAN-Github dataset [41]. However, we did not observe performance improvements and did not include mid-training in the final evaluations. Reinforcement Learning Loop. During RL training, we sample theorems from a corpus of 96,967 autofor- malized statements provided by the NuminaMath-LEAN 7 https://huggingface.co/datasets/nvidia/Nemotron-C-Math-v1, NVIDIA Open Data License dataset [38]. 8 Note that the dataset contains additional 5,529 theorems which are incompatible with Lean v4.27. The RL training was run distributed over a node with eight GPUs and two CPU nodes, with the total hardware requirements detailed in Appendix F (excluding preliminary experiments). 5.1 Results Figure 4 shows the progression of NanoProof success rate on MiniF2F during RL training for different numbers of MCTS iterations, starting with the checkpoint after supervised train- ing. We perform three independent runs of RL training and report the mean score with min/max bands. The runs are independent in terms of both the theorems sampled by the matchmaker and the tactics sampled during node expansion. After 100 steps of RL training, or 45 hours, NanoProof achieves a mean performance of 51.3% on MiniF2F-Valid over 3 runs (min: 51.2%, max: 51.6%) under the budget of 256 MCTS iterations. A final checkpoint, selected from the three using validation split performance, achieves 50.8% pass@16 on MiniF2F-Test under 512 iterations. Our MiniF2F-Test score is contextualized in terms of the total compute budget in Figure 5 relative to selected exist- ing provers. Among the systems of the factorized any-time execution-guided class, NanoProof reaches a higher MiniF2F- Test score than HyperTree Proof Search and ABEL at roughly 90×and 7×less compute, and it is, to our knowledge, the only member of this class whose data, tooling, pipeline, and weights are all released. Open-weight linear provers such as BFS-Prover report higher scores, but they start from a pretrained base model whose pre-training alone costs about 8 https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN, Apache-2.0 License 8 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 three orders of magnitude more than our entire pipeline and cannot be reproduced; NanoProof instead reaches its score training from scratch, within a budget that any research group can rerun and modify. The comparison is necessar- ily heterogeneous in Lean versions, pass@푘protocols, and search budgets, with compute figures converted by us from reported hardware usage, or estimated where it is not dis- closed (Appendix F). 6 Conclusion In this work, we identified and resolved a major roadblock in the open research of a class of automated theorem provers inspired by approaches such as AlphaProof and HyperTree Proof Search. Furthermore, NanoProof, our end-to-end ATP system, reaches a higher MiniF2F-Test score than the previ- ous systems of its class at a fraction of their compute, and is the only one that can be rebuilt from the released artifacts. Along the way, we showcased a synthesis of available public datasets and filled in the missing pieces where necessary, particularly with the introduction of LeanTree, a dataset of structured proof trees extracted from Mathlib, and a tool for efficient distributed interaction with Lean. We release all resulting artifacts as open-source. Limitations. We do not at this time possess enough com- puting resources to fully utilize the presented pipeline, lead- ing to quantitative results that are sub-par compared to Al- phaProof and the open-weight provers of Section 2, and to the absence of proper ablations: only diverse tactic sampling is ablated, while the other search-level techniques are re- ported through descriptive statistics only. We do not claim methodological novelty in the search algorithm, which fol- lows AlphaProof; our contribution lies in the data, tooling, and pipeline that make this class of prover reproducible. The cross-system comparison is heterogeneous in Lean versions, pass@푘protocols, and search budgets, and the compute figures are converted from reported hardware usage or es- timated where undisclosed. NanoProof does not reach the level necessary for IMO or PutnamBench [35] problems, and only MiniF2F is included in the evaluation. Finally, 9.53% of Mathlib proofs are not yet available in a structured format in LeanTree. Acknowledgments This project was supported by the Charles University Grant Agency (GAUK), project no. 458326 and by the grant no. 25-18031S of the Czech Science Foundation (GAČR). This research was partially supported by SVV project number 260 821. We acknowledge VSB – Technical University of Ostrava, IT4Innovations National Supercomputing Center, Czech Republic, for awarding this project access to the LUMI supercomputer, owned by the EuroHPC Joint Undertaking, hosted by CSC (Finland) and the LUMI consortium through the Ministry of Education, Youth and Sports of the Czech Republic through the e-INFRA CZ (grant ID: 90254). This work was supported by the Ministry of Education, Youth and Sports of the Czech Republic through the e-INFRA CZ (ID:90254). References [1]Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. 2024. Pantograph: A Machine-to-Machine Interaction Inter- face for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. arXiv preprint arXiv:2410.16429 (2024). [2]Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. 2025. A Proof-Producing Compiler for Blockchain Ap- plications. J. Autom. Reason. 69, 2 (April 2025), 25 pages. https: //doi.org/10.1007/s10817-025-09723-y [3]Maxwell P Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M Wraback, and Tyler R Josephson. 2024. Formalizing chemical physics using the Lean theorem prover. Digital Discovery 3, 2 (2024), 264–280. [4]Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srini- vas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. 2025. The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. arXiv:2512.07087 [math.RA] https://arxiv.org/abs/2512.07087 [5]Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al.2025. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving. arXiv preprint arXiv:2507.23726 (2025). [6]Lean Community. 2025. Lean 4 REPL. https://github.com/leanprover- community/repl. Accessed: 2025-04-28. [7] Mathlib Community. 2020. The lean mathematical library. In Pro- ceedings of the 9th ACM SIGPLAN International Conference on Cer- tified Programs and Proofs (New Orleans, LA, USA) (CPP 2020). As- sociation for Computing Machinery, New York, NY, USA, 367–381. https://doi.org/10.1145/3372885.3373824 [8]Gérald Doussot. 2024. Cryptography Experiments In Lean 4: SHA-3 Implementation. Cryptology ePrint Archive, Paper 2024/1880. https: //eprint.iacr.org/2024/1880 [9]Jesse Farebrother, Jordi Orbay, Quan Vuong, Adrien Ali Taïga, Yevgen Chebotar, Ted Xiao, Alex Irpan, Sergey Levine, Pablo Samuel Castro, Aleksandra Faust, Aviral Kumar, and Rishabh Agarwal. 2024. Stop Regressing: Training Value Functions via Classification for Scalable Deep RL. arXiv:2403.03950 [cs.LG] https://arxiv.org/abs/2403.03950 [10] Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. 2023. Bal- dur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 1229–1241. [11]Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. 2024. ABEL: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24. [12] Thomas Hales. 2024. The Formal Proof of the Kepler Conjecture: a critical retrospective. arXiv:2402.08032 [math.MG] https://arxiv.org/ abs/2402.08032 [13]Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. 2021. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203 (2021). 9 Matěj Kripner and Milan Straka [14]Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al.2025. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature (2025), 1–3. [15]Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Moham- madamin Barekatain, Simon Schmitt, and David Silver. 2021. Learning and planning in complex action spaces. In International Conference on Machine Learning. PMLR, 4476–4486. [16]Dongwei Jiang, Marcio Fonseca, and Shay B. Cohen. 2024. Lean- Reasoner: Boosting Complex Logical Reasoning with Lean. North American Chapter of the Association for Computational Linguistics (2024). https://doi.org/10.48550/arxiv.2403.13312 [17]Andrej Karpathy. 2025. nanochat: The best ChatGPT that $100 can buy. https://github.com/karpathy/nanochat [18]Evgenia Karunus and Anton Kovsharov. 2024. Paperproof: A new proof interface for Lean 4. https://github.com/Paper-Proof/paperproof Accessed: 2025-04-30. [19]Levente Kocsis and Csaba Szepesvári. 2006. Bandit based monte- carlo planning. In European conference on machine learning. Springer, 282–293. [20]Wouter Kool, Herke Van Hoof, and Max Welling. 2019. Stochastic beams and where to find them: The gumbel-top-k trick for sampling sequences without replacement. In International conference on machine learning. PMLR, 3499–3508. [21]Matěj Kripner, Michal Šustr, and Milan Straka. 2025. LeanTree: Accel- erating White-Box Proof Search with Factorized States in Lean 4. In The 2nd AI for Math Workshop at ICML 2025. arXiv:2507.14722. [22] Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. Advances in neural information processing systems 35 (2022), 26337– 26349. [23]Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, and Dong Yu. 2025. MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation. In Advances in Neural Information Processing Systems. [24]Jannis Limperg and Asta Halkjær From. 2023. Aesop: White-Box Best- First Proof Search for Lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (Boston, MA, USA) (CPP 2023). Association for Computing Machinery, New York, NY, USA, 253–266. https://doi.org/10.1145/3573105.3575671 [25]Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al.2025. Goedel- Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction. arXiv preprint arXiv:2508.03613 (2025). [26]Rabeeh Karimi Mahabadi, Sanjeev Satheesh, Shrimai Prabhumoye, Mostofa Patwary, Mohammad Shoeybi, and Bryan Catanzaro. 2025. Nemotron-c-math: A 133 billion-token-scale high quality math pre- training dataset. arXiv preprint arXiv:2508.15096 (2025). [27]Norman Megill and David A Wheeler. 2019. Metamath: a computer language for mathematical proofs. Lulu. com. [28] Kim Morrison. 2023.lean-training-data: Tools for extracting training-data from Lean libraries. https://github.com/kim-em/lean- training-data. Accessed: 2025-07-01. [29]Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28. Springer, 625–635. [30]Stanislas Polu and Ilya Sutskever. 2020. Generative language model- ing for automated theorem proving. arXiv preprint arXiv:2009.03393 (2020). [31]Alec Radford, Jeff Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. 2019. Language Models are Unsupervised Multitask Learners. (2019). [32]Z Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al.2025. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv preprint arXiv:2504.21801 (2025). [33] David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al.2018. A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play. Science 362, 6419 (2018), 1140–1144. [34]Joseph Tooby-Smith. 2024. Formalization of physics index notation in Lean 4. ArXiv abs/2411.07667 (2024). https://api.semanticscholar.org/ CorpusID:273970152 [35] George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. 2024.Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. arXiv preprint arXiv:2407.11214 (2024). [36] Floris van Doorn, Patrick Massot, and Oliver Nash. 2023. Formalising the h-Principle and Sphere Eversion. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (Boston, MA, USA) (CPP 2023). Association for Computing Machinery, New York, NY, USA, 121–134. https://doi.org/10.1145/3573105.3575 688 [37]Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. Advances in neural information processing systems 30 (2017). [38] Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al.2025. Kimina-Prover Preview: Towards large for- mal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354 (2025). [39]Daniel Whalen. 2016. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644 (2016). [40]Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700 (2024). [41] Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227 (2024). [42]Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024. Deepseek- prover: Advancing theorem proving in llms through large-scale syn- thetic data. arXiv preprint arXiv:2405.14333 (2024). [43]Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Ming Ding. 2025. BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. In Proceedings of the 63rd Annual Meeting of the Association for Computa- tional Linguistics (Volume 1: Long Papers). [44] Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan, and Xia Xiao. 2025. Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers. arXiv preprint arXiv:2509.06493 (2025). [45]Linting Xue, Aditya Barua, Noah Constant, Rami Al-Rfou, Sharan Narang, Mihir Kale, Adam Roberts, and Colin Raffel. 2022. ByT5: Towards a token-free future with pre-trained byte-to-byte models. arXiv:2105.13626 [cs.CL] https://arxiv.org/abs/2105.13626 [46]An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chengyuan Li, Dayiheng Liu, Fei Huang, Haoran Wei, et al.2024. Qwen2.5 Technical Report. arXiv preprint arXiv:2412.15115 (2024). 10 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 [47]Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems 36 (2023), 21573–21612. [48]Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847 (2024). [49]Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. 2024. Internlm-math: Open math large language models toward veri- fiable reasoning. arXiv preprint arXiv:2402.06332 (2024). [50]Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110 (2021). 11 Matěj Kripner and Milan Straka A Preliminaries: Lean and Proof Search In Lean, theorem statements correspond to types and proofs correspond to values. Theorem proving then amounts to producing a term whose type is equal to the theorem type. For example, consider the following theorem: theorem sub_zero (a b : N) (h : b = 0) : a - b = a (3) Proving Theorem 3 consists in supplying a term of typea - b = a using the available free variablesa,bof typeNandhof typeb = 0. While such a term can be written down explicitly, it is common to utilize Lean’s tactic mode to structure the proof in a format more aligned with human-written proofs. Upon entering tactic mode using thebykeyword, Lean creates a metavariable with the desired typea - b = aand no value assigned yet. Metavariables can be thought of as holes in a proof that have to be filled in before the proof is considered finished. This gives us an intermediate state in the proof construction, where the proof term is type-correct but still contains holes to be filled in later. The still unassigned metavariables are called open goals, so each goal has a target type and a set of available free variables called hypotheses. Because goals are metavariables, the two terms are often used interchangeably. We then proceed by applying a tactic to the list of open goals. A tactic is a procedure that assigns values to one or more open goals, with each of the values possibly containing new unassigned metavariables. In this way, a tactic invoca- tion transforms the list of open goals into a new list of open goals. Typically, a tactic only affects the main goal (defined to be the first goal), either solving it or reducing it to one or more simpler sub-goals. The proof is finished once there are no more open goals, i.e., every metavariable has been assigned. Proof State Factorization. We follow Lample et al. [22]in factorizing proof states into independent goals, which can be explored and proven individually. Note that we temporarily disregard metavariable coupling, which is addressed later in this section. An example of potential state reuse is shown in Figure 6, where the same node is reached using two different search paths. theorem mul_eq_zero_iff (n m : N) : n * m = 0 ↔ n = 0 ∨ m = 0 (4) A possible strategy to prove Theorem 4 is to branch out based on the values of푛and푚. We achieve this by executing the tacticcases n <;> cases m. Since each of the two numbers can be either zero or a successor of another number, the resulting proof state consists of four goals. For example, one of the states is(푛 ′ +1) ·0=0↔ 푛 ′ +1=0∨0=0, corresponding to the case where푛is a successor and푚is zero. To complete the proof, all four goals must be closed. In a non-factorized setting, the proof state consisting of four goals is assessed by the policy and critic models as a whole. Since tactics typically affect only the main goal, the last goal can only be worked on once all others have been closed. In contrast, factorized states allow the search algorithm to focus on the goals individually, in any order the algorithm deems fit. AND-OR Search. The search of factorized states naturally yields an AND-OR tree, where a prover selects a tactic in an OR node and subsequently has to prove all the goals in an AND node. Figure 6 shows an example in which choosing either therwtactic or thecasestactic in the root leads to a proof. For a more in-depth introduction to proof search in Lean, refer to [24]. Metavariable Coupling. It is not always possible to fully factorize the proof state into individual goals that can be proven independently. For this reason, nodes in the proof tree are allowed to contain more than one goal. Specifically, this occurs when two goals share the same metavariable – for example, applying the transitivity lemmaNat.le_trans to the goal 2≤5 produces goals 2≤ ?mand?m≤5 sharing a metavariable?mwhose value has not yet been decided. 9 Subsequently, choosing a value for?min one of the goals affects the provability of the other goal, and therefore the two goals cannot be explored independently. For a more in-depth explanation of this phenomenon, we recommend Aniva et al. [1]. B Hyperparameter Overview We give an overview of the most notable hyperparameters used during training and search in Table 1. C Proof Simplification We provide an example of a proof found during the RL train- ing loop in Listing 5 and its simplified version in Listing 6. The latter was produced by the simplification algorithm de- scribed in Section 3.5. Only the simplified version is saved to the replay buffer during training. 9 A third goal of type N is created for technical reasons. 12 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 ORORANDAND ⊢ a - 0 = a h : b’ + 1 = 0 ⊢ a - (b’ + 1) = a h : b = 0 ⊢ a - b = a ⊢ a - 0 = a rw [Nat.sub_zero] rw [Nat.sub_zero] contradiction rw [h] cases b Figure 6. Example of an AND-OR proof tree for Theorem 3. Nodes connected with a dashed line could potentially be merged and correspond to transpositions in games. This is possible thanks to factorization. Table 1. Architectural, optimization and search hyperparameters. CategoryHyperparameterValue Prover Network Total Parameters1B Number of Blocks26 푑 푚표푑푒푙 1664 Attention Heads13 Feed Forward Widening Factor4 Vocabulary Size50,441 RoPE Base (휃 )100,000 Value Bins1, 2, . . ., 64 Pre-Training Sequence Length768 Global Batch Size491,520 AdamW Betas(0.8, 0.95) AdamW Epsilon1× 10 −10 Muon Momentum0.97 LR (embedding)0.3· 1/ √︁ 푑 푚표푑푒푙 /768 LR (unembedding)0.008· 1/ √︁ 푑 푚표푑푒푙 /768 LR (matrices)0.02 LR Warmdownlast 65% Fine-TuningValue Weight0.01 RL Training Replay Buffer Max. Size250k transitions Supervised Data Fraction10% Transitions per Step (푛 samples )100 Examples per Update Step256 Updates per Step (푛 updates )2 푛 sim during Experience Collection64 Proof Search Maximum Tactic Length24 tokens Sampled Tactics6 Progressive Sampling퐶0.1 Progressive Sampling 훼0.6 UCB value discount 훽0.98 UCB prior temperature 휏200 UCB exploration constant 푐 푖푛푖푡 0.001 UCB exploration constant 푐 푏푎푠푒 200 UCB AND-node prior multiplier 푐 퐴푁퐷 64 UCB unvisited children value penalty16 13 Matěj Kripner and Milan Straka theorem algebra_2complexrootspoly_xsqp49eqxp7itxpn7i (x : C) : x 2 + 49 = (x + 7 * Complex.I) * (x + -7 * Complex.I) := by subst_vars rw [← sub_eq_zero] rw [← sub_eq_zero] simp simp only [Real.cos_sq, Real.sin_sq, mul_comm, neg_mul] rw [sub_eq_add_neg] rw [mul_comm] rw [pow_two] rw [← sub_eq_zero] simp only [mul_comm] simp [sub_eq_add_neg] rw [add_comm] rw [← sub_eq_add_neg] rw [mul_comm] rw [mul_add] rw [sub_eq_add_neg] simp_all rw [add_comm] rw [← sub_eq_zero] rw [← neg_sub] rw [add_comm] rw [← neg_add] rw [sub_eq_add_neg] rw [← sub_self] rw [← neg_neg x] rw [sub_neg_eq_add] rw [neg_mul] rw [add_comm] ring_nf norm_num (5) theorem algebra_2complexrootspoly_xsqp49eqxp7itxpn7i' (x : C) : x 2 + 49 = (x + 7 * Complex.I) * (x + -7 * Complex.I) := by rw [← sub_eq_zero] ring_nf norm_num (6) D Structured Proof Tree Extraction Figures 7 and 8 provide proof trees presented schematically in Figure 3. E Incremental Proof Verification Originally, the Lean REPL did not utilize the Lean verifica- tion kernel to type-check assignments introduced by tactic applications, leading to incorrect proofs being accepted in some cases. Our prover managed to exploit these inconsis- tencies, finding 12 incorrect proofs in the MiniF2F validation set that passed verification in the REPL when using the tactic mode. One of these incorrect proofs is listed below. theorem mathd_algebra_422 (x : R) (휎 : Equiv R R) (h 0 : ∀ x, 휎.1 x = 5 * x - 12) (h 1 : 휎.1 (x + 1) = 휎.2 x) : x = 47 / 24 := by rw [h 0 ] at h 1 by_contra! h apply h.symm simpa using h _ Lean correctly rejects the above proof with the error: “don’t know how to synthesize placeholder”. However, when executing the proof in the tactic mode using the old version of Lean REPL, the proof passes as correct. In a recent update, 10 Lean REPL was extended to type- check the full proof term after each tactic application, miti- gating all false positives in the verification process, at the cost of introducing some drawbacks detailed below. We propose a different strategy: Instead of verifying the type-correctness of the whole proof term, type-check only the new assign- ments introduced by a tactic application. To illustrate this difference, assume that we are searching for a proof of type푇and have already constructed a term 푡:푇which still contains unassigned metavariables of types 퐺 1 , . . .,퐺 푛 . Next, assume that we apply a tactic assigning terms푔 1 :퐺 1 , . . .,푔 푛 :퐺 푛 to the metavariables in푡. The current strategy of Lean REPL is to type-check the whole assignment푡:푇, which contains the new terms푔 1 , . . .,푔 푛 as subterms. This leads to issues when the proof bifurcates into two branches. For example, consider applying the tactichave k := sorryin the REPL’s tactic mode. 11 This corresponds to the assignment of the term((fun k ↦→ ?_) sorry)to the metavariable corresponding to the main goal, where?_ is a new unassigned metavariable. Lean REPL then enables solving the?_andsorryparts independently. However, assignments made in one of these two branches are not prop- agated to the other one, meaning that, from the perspective of each branch, the root proof term will always contain at least one hole introduced by an unassigned metavariable or thesorrykeyword. This leads to the kernel always failing during a type check for the duration of this proof. The end effect is that the current verification strategy leads to false 10 Published on GitHub on Apr 10, 2025. 11 This is the standard way to use thehavetactic in the REPL – see for example https://github.com/leanprover-community/repl/blob/master/tes t/have_by_sorry.in 14 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 theorem succ_less_double_succ (n : Nat) : n > 0 → n < 2 * n := by intro h cases n with | zero => apply h | succ n' => apply Nat.le_trans case m => exact n' + 2 · rfl · rw [two_mul, add_succ] have h1 : 1 ≤ n' + 1 · apply Nat.succ_le_succ (Nat.zero_le _) · exact Nat.add_le_add_left h1 (n' + 1) ⊢ n > 0 → n < 2 * n intro h h : n > 0 ⊢ n < 2 * n cases n case zero h : 0 > 0 ⊢ 0 < 2 * 0 case succ h : n✝ + 1 > 0 ⊢ n✝ + 1 < 2 * (n✝ + 1) case succ n' h : n' + 1 > 0 ⊢ n' + 1 < 2 * (n' + 1) apply Nat.le_trans h : n' + 1 > 0 ⊢ (n' + 1).succ ≤ ?m ⊢ ?m ≤ 2 * (n' + 1) ⊢ ℕ case m => exact n' + 2 h : n' + 1 > 0 ⊢ (n' + 1).succ ≤ n' + 2 h : n' + 1 > 0 ⊢ n' + 2 ≤ 2 * (n' + 1) rfl have h1 : 1 ≤ n' + 1 h : n' + 1 > 0 ⊢ 1 ≤ n' + 1 h : n' + 1 > 0 h1 : 1 ≤ n' + 1 ⊢ (n' + 1).succ ≤ n' + 1 + (n' + 1) apply h · · Figure 7. Example Lean theorem and its corresponding executable proof tree extracted using LeanTree. Some tactics and hypotheses are omitted. negatives when the proof being verified contains at least one syntactic branching. In contrast, the proposed strategy implemented in LeanTree type-checks only the new assignments푔 1 : 퐺 1 , . . .,푔 푛 :퐺 푛 introduced by a tactic application. The type correctness of the whole proof term푡:푇then follows transitively. Most importantly, this new verification strategy mitigates the false negatives described in the previous paragraph. Additionally, the new strategy also decreases the time complexity of verifying a proof from quadratic to linear since each sub-assignment is only verified once. Note that all proofs found by our prover are independently verified directly using Lean, bypassing Lean REPL together with the new verification algorithm described in this section. F Compute Estimation Methodology We estimate compute in FLOPs based on reported hardware usage, training time, and the following approximate conver- sion factors for BF16: •NVIDIA H100 NVL: 1671 TFLOPS •NVIDIA A100: 312 TFLOPS •NVIDIA L40: 242 TFLOPS •NVIDIA V100: 125 TFLOPS 15 Matěj Kripner and Milan Straka theorem tsub_eq_tsub_of_add_eq_add (h : a + d = c + b) : a - b = c - d := by calc a - b = a + d - d - b := by rw [add_tsub_cancel_right] _ = c + b - b - d := by rw [h, tsub_right_comm] _ = c - d := by rw [add_tsub_cancel_right] h : a + d = c + b ⊢ a - b = c - d h : a + d = c + b h1 : a - b = a + d - d - b ⊢ a - b = c - d have h1 : a - b = a + d - d - b have h2 : a + d - d - b = c + b - b - d h : a + d = c + b h1 : a - b = a + d - d - b h2 : a + d - d - b = c + b - b - d ⊢ a - b = c - d · exact Trans.trans h1 (Trans.trans h2 h3) h : a + d = c + b ⊢ a - b = a + d - d - b rw [add_tsub_cancel_right] h : a + d = c + b h1 : a - b = a + d - d - b ⊢ a - b = a + d - d - b rw [h, tsub_right_comm] Figure 8. Example Lean theorem and its corresponding executable proof tree extracted using LeanTree. Some tactics and hypotheses are omitted. •Google TPU v6e (used in AlphaProof ): 918 TFLOPS •AMD Instinct MI250: 383 TFLOPS Note that this form of compute budget estimation only provides rough estimates since the precise hardware charac- teristics and architectural details are not taken into consid- eration. Per-Model Estimation Details AlphaProof [14]: Computational budget as reported in- cludes 10 TPUdays for base training, 100,000 TPUdays for the autoformalization process, 80,000 TPUdays for RL train- ing, and 500 TPUdays per problem for TTRL. These 302,010 TPUdays (with test set size 244) correspond approximately to 2.4×10 13 TFLOPs. Of this budget, 100,000 TPUdays are spent on autoformalization. NanoProof does not perform autofor- malization but consumes the NuminaMath-LEAN corpus, whose generation cost is not disclosed and not included in our total. Relative to NanoProof’s 3.8× 10 8 TFLOPs, the ra- tio is approximately 63,000×for AlphaProof’s total budget, 42,000×when its autoformalization stage is excluded, and 17,000×when counting only its RL stage; we therefore state the difference conservatively as more than four orders of magnitude. HyperTree Proof Search (HTPS) [22]: Compute budget as reported is 1260 A100-days for training with negligible inference cost. This approximately corresponds to 3.4×10 10 TFLOPs. ABEL [11]: Compute budget as reported is 96 A100-days for training with negligible inference cost. This approxi- mately corresponds to 2.6× 10 9 TFLOPs. DeepSeek-Prover-V2 [32]: Because the compute budget of DeepSeek-Prover-V2 has not been disclosed, we estimate it as approximately 10 13 TFLOPs based on its architecture and training methodology: it fine-tunes a 671B parameter model using RL over a large formal proof dataset with recursive self-play. The estimate is conservatively aligned with models of similar size and RL complexity. ReProver [47]: The training of retrieval and policy mod- els requires 5 A100-days, corresponding to 1.3×10 8 TFLOPs. Inference then requires 16 V100-days, corresponding to 1.7×10 8 TFLOPs. However, the training was initialized from Google ByT5 Small [45], which required an estimate of 10 9 TFLOPs. We thus report the total approximate budget as 1.3× 10 9 TFLOPs. BFS-Prover [43]: The prover is fine-tuned from Qwen2.5- Math-7B, and its fine-tuning compute is not fully disclosed. We therefore report a lower bound given by the pre-training cost of the base model alone, estimated as 6푁퐷for푁parame- ters and퐷training tokens, with 18T tokens for Qwen2.5 [46], giving approximately 7.6× 10 11 TFLOPs. NanoProof: Here we describe one final run of NanoProof. Supervised training, consisting of base training and fine- tuning, was performed on four A100-SXM4-40GB GPUs for a total of 16.3 hours. RL training was performed on four AMD Instinct MI250 accelerators (each exposing two GPU devices, i.e., the eight GPUs of Section 5) for 45 hours together with two CPU nodes with comparatively negligible TFLOPS. The final pass@16 performance was evaluated on four AMD Instinct MI250 GPUs for 11 hours. This approximately corresponds to 7.3×10 7 TFLOPs for supervised training, 2.5×10 8 TFLOPs for RL, and 6.1×10 7 16 NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 TFLOPs for final evaluation, for a total of 3.8×10 8 TFLOPs. Note that this total includes the final evaluation (6.1×10 7 TFLOPs, 16%), while the figures for HyperTree Proof Search and ABEL cover training only. G LeanTree Comparison to Existing Tools Several tools have recently emerged for both programmatic interaction with Lean and machine learning data extraction from human-written Lean proofs. In this section, we compare them to LeanTree. We argue that LeanTree brings novel unique extraction capabilities. Evariste [22] corresponds most closely to LeanTree. Evariste enables factorizing proof state into individual goals, which can be explored independently. In addition, Evariste detects metavariable coupling and does not split metavariable-dependent goals, similar to LeanTree. However, the Evariste dataset has not been released and the tool itself is available only in a limited, nonexecutable for- mat. 12 This makes it challenging to build on top of Evariste’s contributions. Importantly, Evariste was only implemented for Lean 3, which is now deprecated. Since its core logic is implemented using C++, directly binding to Lean 3 internals, its migration to Lean 4 would be difficult. In contrast, the core logic of LeanTree is implemented in Lean 4 itself, which is a common Lean 4 paradigm [29]. Furthermore, LeanTree builds on top of the semi-official Lean REPL project, and it is therefore set to benefit from future improvements by the community. LeanDojo [47] offers both an interaction module and a supervised data extraction module. The extracted data also contains information about the premises used in each tactic application, enabling training of retrieval-augmented generation models. The extracted datasets are available for both Lean 3 and Lean 4. However, LeanDojo does not offer proof state factoriza- tion, tactic simplification, or proof tree building. First, this means that a tactic can only be applied to a whole proof state consisting of a list of goals, yielding a new set of goals. This prevents parallel search over independent goals. Second, tactics in the LeanDojo dataset are left in the form in which they appear in the abstract syntax tree of a Lean source code. This includes complex or nested tactics that span multiple lines. For example, thecasestactic shown in Figure 7 is left unaltered. The user of the dataset can then choose to filter out such samples, losing valuable training data, or keep them in the training set, but increase the diffi- culty of the modeling task and reduce the granularity of the inference-time proof search. 12 Specifically, the codebase states: “code does NOT run out of the box as we removed references to Meta-internal systems” https://github.com/faceb ookresearch/Evariste Third, LeanDojo does not contain information about the sub-proof size and sub-proof depth for each node, and pro- vides tactics in an unstructured format that is not conducive to proof tree building. Pantograph [1] In contrast to LeanDojo, Pantograph’s interaction and data extraction modules offer proof state fac- torization, meaning that independent goals can be explored independently. Pantograph also provides information about which goals are coupled via a shared metavariable. However, tactic simplification and proof tree building are not supported by the data extraction module, leading to the same drawbacks as described for the case of LeanDojo. Information about sub-proof size and sub-proof depth is also not provided. In addition, the Pantograph API is not well suited for gradually building the current Lean context by interleaving definitions and theorems that can depend on any previously declared ones. Instead, theorems are treated as independent units. H Dataset Schema Each sample in the LeanTree dataset corresponds to a Lean file rather than just an individual theorem. This is necessary to capture the structure of a real-world Lean project like Mathlib where a proof can depend on any definition located above it in the source file. Each file in the dataset contains a list of theorems, and each theorem contains a list of all tactic proofs in its proof term. Note that there can be more than one tactic proof for a theorem if its proof contains more than one non-nested by-blocks. For each tactic proof, the dataset then contains a proof tree with nodes corresponding to factorized proof states and edges corresponding to tactic applications. Every proof node contains also precomputed size and the depth of its sub-tree. Additionally, the LeanTree dataset contains information about the surrounding context, namely the list of imported modules for each Lean file and the list of open namespaces for each theorem. The correspondence between samples in the dataset and the underlying Lean repository is given by character offsets specifying the span of each theorem, proof, and tactic execution. The JSON schema of the dataset is presented in Figure 9. 17 Matěj Kripner and Milan Straka 1 <sample > ::= 2 "path": <string >, 3 "imports": [<string >], 4 "theorems": [<theorem >] 5 6 7 <theorem > ::= 8 "span": <span?>, 9 "name": <string?>, 10 "context": [<string >], 11 "by_blocks": [<by_block >], 12 "error": <string?> 13 14 15 <by_block > ::= 16 "span": <span >, 17 "tree": 18 "nodes": [<proof_node >], 19 "root_id": <string?>, 20 "error": <string?> 21 22 23 24 <proof_node > ::= 25 "id": <string >, 26 "state": 27 "goals": [<goal >] 28 , 29 "tactic": <edge?>, 30 "proof_size": <int?>, 31 "proof_depth": <int?> 32 33 34 <edge > ::= 35 "tactic_string": <string >, 36 "span": <span?>, 37 "parent": <string >, 38 "children": [<string >], 39 "tactic_depends_on": [<string >?] 40 41 42 <goal > ::= 43 "type": <string >, 44 "hypotheses": [<hypothesis >], 45 "tag": <string >? 46 47 48 <hypothesis > ::= 49 "type": <string >, 50 "user_name": <string >, 51 "value": <string >? 52 53 54 <span > ::= 55 "start": <int >, 56 "finish": <int > 57 Figure 9. JSON schema of a sample in the LeanTree dataset. 18