PaperlayerView exact revision on arXiv

Source-linked AI summary

NanoProof: Open and Efficient Automated Theorem Proving in Lean 4

Matěj Kripner, Milan Straka

arXiv:2610.11605v1cs.LGcs.AI

TL;DR

Factorized execution-guided theorem provers need structured training data and verifier integration, but prior systems in this class did not release data or runnable code. NanoProof releases a Lean 4 prover, proof-tree data, extraction tooling, and training pipeline; it reaches 50.8% pass@16 on MiniF2F-Test with substantially less compute than AlphaProof.

  • Problem

    Factorized execution-guided provers require structured training data and verifier integration, yet prior systems of this class released neither their data nor runnable code.

    Source: §1 · p. 2

  • Method

    NanoProof releases a factorized execution-guided prover, LeanTree structured proof trees, extraction tooling, and the artifacts needed to reproduce the system.

    Source: §1 · p. 2

  • Results

    50.8% pass@16 on MiniF2F-Test was achieved using more than four orders of magnitude less compute than AlphaProof.

    Source: §1 · p. 2

  • Takeaways & Limitations

    NanoProof reaches a higher MiniF2F-Test score than prior systems of its class at a fraction of their compute and can be rebuilt from released artifacts.

    Source: §6 · p. 9

    The authors lack enough compute to fully use the pipeline, leaving most search-level techniques without proper ablations and making cross-system comparisons heterogeneous.

    Source: §6 · p. 9

Abstract

from arXiv · show

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.

1 Introduction

Factorized execution-guided theorem provers can use verifier feedback and independently search proof branches, but their data and runnable systems have been unavailable to the open-source community. NanoProof addresses this reproducibility barrier with an open Lean 4 pipeline, released proof-tree data and tooling, and a 50.8% pass@16 MiniF2F-Test result.

1 Introduction

  • Formal verification can automatically filter incorrect solutions, and formalized results can expedite review and support large collaborative mathematics projects.The introduction connects this role to anticipated growth in AI-generated code, proofs, and other artifacts.Source: §1 · p. 1
  • Execution-guided provers condition each step on verifier feedback and the current proof state, unlike execution-agnostic systems that verify only the final proof.Without this feedback, the proof-step generator must infer the evolving state, coupling policy and world modeling.Source: §1 · p. 1
  • Factorized search can explore proof branches independently, while any-time search can use results across searches as compute increases.For example, induction separates base and inductive cases, enabling parallelization and dynamic allocation of search budget between branches.Source: §1 · p. 1
  • Existing factorized execution-guided systems released neither their data nor runnable code, leaving this prover class out of reach for open-source research.The paper identifies those reproducibility barriers as a roadblock to studying search-based provers alongside large language models.Source: §1 · pp. 1–2
  • NanoProof releases a factorized any-time execution-guided prover, its reproduction tooling, and LeanTree, with 92,927 independently verified structured proof trees.The release also includes an extraction tool for Lean 4 projects and an interface with incremental kernel verification and a distributed environment pool for reinforcement learning.Source: §1 · p. 2
  • 50.8% pass@16 on MiniF2F-Test was achieved using more than four orders of magnitude less compute than AlphaProof.The introduction also reports search-level techniques and quantifies their effects where the compute budget allowed.Source: §1 · p. 2

2 Related Work

Prior work spans text-to-text and execution-guided theorem proving, while the open execution-guided provers described here search linear monolithic states. Existing proof datasets provide useful Lean material but do not supply the structured, simplified proofs and distance-to-proof-end information needed for NanoProof training.

2 Related Work

  • Lean 4's extensibility lets users modify its syntax and semantics, a property the authors heavily use in LeanTree.Mathlib and community formalization projects provide human-written material for supervised theorem-prover training.Source: §2 · pp. 2–3
  • Goedel-Prover-V2 reports 88.1% on MiniF2F-Test at pass@32, while Seed-Prover reports 99.6%.These are text-to-text approaches using large language models, including chain-of-thought refined with reinforcement learning.Source: §2 · p. 2
  • Open execution-guided provers such as BFS-Prover and MPS-Prover use linear best-first search over monolithic Lean proof states, not factorized search.They release at most weights and inference code, not training data or pipeline; their reported budgets exclude base-model pretraining.Source: §2 · p. 3
  • The comparison between large pretrained policies and factorized search with a trained critic remains an open question.The paper notes that the open release makes this question testable.Source: §2 · p. 3
  • Existing Lean datasets lack tactic proofs in a structured, simplified format and do not include distance-to-proof-end information required for NanoProof training.LeanDojo adds premise information for retrieval-augmented training, while related datasets include Pantograph and lean-training-data.Source: §2 · p. 3

3 NanoProof Automated Theorem Prover

NanoProof combines factorized proof search with a staged training pipeline and Lean integration. Its implementation adds proof simplification, augmentation, cycle detection, and diverse tactic sampling.

3 NanoProof Automated Theorem Prover

  • The prover's training and inference mechanism relies on LeanTree's structured proof-tree dataset and extraction tool for supervised training.The paper presents its proof-search algorithm as mostly following Hubert et al., with later sections describing implementation choices and additions.Source: §3 · p. 3

3.1 Proof Search Algorithm

  • The proof-search agent observes open goals, applies Lean tactics, and receives resulting states; completed proof trees are rewarded according to their depth.The search uses an actor for tactic prediction, a critic for future reward, and an AND-OR tree expanded through selection, expansion, and backpropagation.Source: §3.1 · pp. 3–4

3.2 Network Architecture

  • A single Transformer models actor and critic behavior, predicting tactics autoregressively and critic values in one forward pass.The model uses shared vocabulary rather than dedicated actor and critic heads.Source: §3.2 · p. 4

3.3 Training Pipeline

  • Supervised training progresses from general math-related text through Lean source code to increasingly targeted human-authored proof data before self-improvement.During self-improvement, successful proof transitions enter a replay buffer for further training, mixed with some supervised fine-tuning data for stability.Source: §3.3 · p. 4

3.4 Lean Integration

  • LeanTree exposes Lean REPL interaction and maintains a dynamic pool of environments over HTTP for deployment to CPU nodes.It supports restarting from intermediate proof states for tree search and backtracking; found proofs are independently verified as standalone Lean code.Source: §3.4 · p. 4

3.5 Proof Simplification and Augmentation

  • Proof simplification removes redundant tactics when contracting an edge preserves proof validity, and proof augmentation randomly renames or shuffles hypotheses and goals.In a representative run, the simplifier reduced 59% of proofs longer than one tactic.Source: §3.5 · pp. 4–5

3.6 Cycle Detection

  • Cycle detection discards tactics that recreate a goal already on the path to the root, checking equivalence up to reshuffling, renaming, and whitespace.In a representative run, 18% of otherwise valid tactics were rejected.Source: §3.6 · p. 5

3.7 Diverse Tactic Sampling

  • Diverse tactic sampling uses the Gumbel-Top-k trick to cap occurrences of first tokens and reduce duplicate tactic samples.It increased MiniF2F-Valid performance by 2.0 percentage points under 16 simulations, averaged over the last three saved checkpoints in one run.Source: §3.7 · p. 5

4 Structured Proof Tree Dataset

LeanTree converts compact human-written Lean proofs into incrementally structured proof trees that support factorized search, while verifying extracted trees through Lean.

4 Structured Proof Tree Dataset

  • Dynamic tactic combinators, multi-goal operators, goal reordering, and metavariable coupling complicate turning Lean's linear scripts into independently searchable trees.The extraction challenge also reflects the difference between compact human-written proofs and the small incremental steps suited to search.Source: §4 · p. 5
  • LeanTree contains 92,927 extracted proof trees from a recent version of Mathlib, each independently verified; 9.53% of Mathlib tactic proofs were excluded because all tactics in their extracted trees could not be verified.Source: §4 · p. 5

4.1 Singleton Tree Construction

  • LeanTree builds singleton trees by matching tactic applications to affected goals, using Lean REPL with an augmented BetterParser module.A tactic can transform a list of open goals into a new list without additional guarantees, making this mapping nontrivial.Source: §4.1 · p. 6

4.2 Tactic Simplification

  • Complex tactics are simplified by extracting nested tactic blocks, decomposing calc chains, separating cases or induction branches, and splitting merged rw tactics.Each resulting tactic is intended to be a valid, self-contained proof step.Source: §4.2 · p. 6

4.3 Merging Metavariable-Dependent Goals

  • Sibling nodes sharing a metavariable are merged, and the resulting tree is executed from the root; trees that fail verification are excluded.Once a metavariable is assigned, remaining goals may become independent and can be split.Source: §4.3 · p. 7

5 Experiments

NanoProof's final checkpoint achieved 50.8% pass@16 on MiniF2F-Test, outperforming two comparable factorized provers at substantially lower compute; the reported comparison is heterogeneous. The system was trained through supervised phases followed by reinforcement learning.

5 Experiments

  • Training used 10B Nemotron-CC-Math-4+ tokens, then 258k LeanTree proof steps, followed by reinforcement learning on 96,967 NuminaMath-LEAN theorems.The proof-step fine-tuning set comprised 287k steps, with the final 10% of files held out for validation.Source: §5 · p. 8

5.1 Results

  • 50.8% pass@16 on MiniF2F-Test; NanoProof scored higher than HyperTree Proof Search and ABEL at roughly 90× and 7× less compute, respectively.The final checkpoint was selected by validation performance and evaluated under 512 iterations.Source: Figure 5 · p. 8, §5.1 · p. 8
  • The prover reached 51.3% mean MiniF2F-Valid performance after 100 RL steps or 45 hours, over three runs using 256 MCTS iterations.The reported range across runs was 51.2% to 51.6%.Source: §5.1 · p. 8
  • The cross-system comparison is heterogeneous across Lean versions, pass@k protocols, and search budgets, and some compute figures are converted or estimated.The authors state that compute figures were converted from reported hardware usage or estimated when undisclosed.Source: §5.1 · p. 9

6 Conclusion

NanoProof makes a class of factorized execution-guided theorem provers reproducible through released data, tools, and pipeline artifacts. Its MiniF2F-Test result exceeds earlier systems of its class at lower compute, while the paper identifies resource, evaluation, and coverage limits.

6 Conclusion

  • NanoProof reaches a higher MiniF2F-Test score than previous systems of its class at a fraction of their compute, and can be rebuilt from released artifacts.The paper identifies its contribution as making this prover class reproducible, rather than introducing a novel search algorithm.Source: §6 · p. 9
  • LeanTree provides structured proof trees extracted from Mathlib, alongside a tool for extraction and efficient distributed interaction with Lean.The authors report releasing the resulting artifacts as open source.Source: §6 · p. 9
  • Evaluation is limited to MiniF2F, and NanoProof does not reach the level needed for IMO or PutnamBench problems.The authors also report insufficient compute for fully using the pipeline and proper ablations; 9.53% of Mathlib proofs are not yet structured in LeanTree.Source: §6 · p. 9

A Preliminaries: Lean and Proof Search

Lean represents theorem statements as types and proofs as values, while tactic mode advances a proof by transforming open goals. The section explains how factorization enables independent exploration, with metavariable coupling limiting when goals can be separated.

A Preliminaries: Lean and Proof Search

  • Lean’s theorem statements are types and proofs are values; in tactic mode, open goals are metavariables that tactics transform until every goal is assigned.Each goal has a target type and available hypotheses, and a proof is finished when no open goals remain.Source: A Preliminaries: Lean and Proof Search · p. 12
  • Figure 6 illustrates possible state reuse when different search paths reach the same node.The figure caption says dashed-linked nodes could be merged and correspond to game transpositions, enabled by factorization.Source: A Preliminaries: Lean and Proof Search · p. 12
  • Factorized proof states let search work on separate goals individually and in any order, rather than waiting for earlier goals to close.The example branches on two natural numbers into four goals; a non-factorized search assesses them together.Source: A Preliminaries: Lean and Proof Search · p. 12
  • An AND-OR proof tree has tactic choices at OR nodes and requires all resulting goals to be proved at AND nodes.Goals sharing a metavariable cannot be explored independently because assigning it in one affects the other.Source: A Preliminaries: Lean and Proof Search · p. 12

B Hyperparameter Overview

  • Table 1 overviews notable hyperparameters used during training and search.Its caption identifies architectural, optimization, and search hyperparameters as the table’s scope.Source: B Hyperparameter Overview · p. 12

C Proof Simplification

The section presents proof simplification in the training loop and relates examples of structured proof trees to the paper’s schematic tree figure.

C Proof Simplification

  • Only the simplified version of an example proof is saved to the replay buffer during RL training.The simplified proof is produced by the algorithm described in Section 3.5.Source: C Proof Simplification · p. 12
  • Figure 6 shows an AND-OR proof tree whose dashed-linked nodes could be merged as transpositions, a possibility attributed to factorization.The passage describes this as an example for Theorem 3.Source: Figure 6 · p. 13

D Structured Proof Tree Extraction

E Incremental Proof Verification

The section describes false positives in an earlier Lean REPL verification strategy and a LeanTree alternative that checks only assignments introduced by each tactic. The proposed strategy mitigates branch-related false negatives and reduces verification time complexity from quadratic to linear.

E Incremental Proof Verification

  • The old REPL accepted 12 incorrect MiniF2F validation proofs, while a recent update type-checks the full proof term after each tactic application.The authors independently verify their prover’s proofs directly with Lean, bypassing the REPL.Source: E Incremental Proof Verification · pp. 14–15
  • Full-term checking can fail during syntactically branching proofs because assignments in separate branches are not propagated to one another.The resulting unassigned metavariable or sorry can make the kernel fail its type check throughout the proof.Source: E Incremental Proof Verification · p. 14
  • Checking only new assignments makes proof-term correctness follow transitively and reduces verification time complexity from quadratic to linear.The authors say each sub-assignment is verified only once.Source: E Incremental Proof Verification · p. 15
  • The proposed assignment-level strategy mitigates the false negatives associated with branching proofs.Source: E Incremental Proof Verification · pp. 14–15

F Compute Estimation Methodology

The compute estimates convert reported hardware usage and training time into approximate FLOPs, using hardware-specific BF16 conversion factors. The appendix gives per-model budgets and notes that comparisons are approximate and may cover different stages.

Compute Estimation Methodology

  • The conversion uses approximate BF16 hardware throughput values, and the authors caution that estimates omit precise hardware characteristics and architectural details.Listed examples include 312 TFLOPS for an A100 and 383 TFLOPS for an AMD Instinct MI250.Source: F Compute Estimation Methodology · pp. 15–16

Per-Model Estimation Details

  • 2.4×10^13 TFLOPs is the estimated AlphaProof budget, about 63,000× NanoProof’s 3.8 × 10^8 TFLOPs, or 42,000× excluding autoformalization.The AlphaProof estimate includes autoformalization, which accounts for 100,000 TPU-days; NanoProof’s total excludes undisclosed NuminaMath-LEAN corpus generation costs.Source: Per-Model Estimation Details · p. 16
  • 3.4 × 10^10 TFLOPs is the estimated HTPS training budget, compared with 2.6 × 10^9 TFLOPs for ABEL.The estimates are based on reported training usage and convert 1260 A100-days for HTPS and 96 A100-days for ABEL.Source: Per-Model Estimation Details · p. 16
  • The appendix estimates DeepSeek-Prover-V2 at approximately 10^13 TFLOPs and reports ReProver at approximately 1.3 × 10^9 TFLOPs, including base-model initialization.DeepSeek’s undisclosed budget is estimated from its architecture and training methodology; ReProver’s reported total includes an estimate for ByT5 Small pretraining.Source: Per-Model Estimation Details · p. 16
  • 3.8 × 10^8 TFLOPs is NanoProof’s estimated total, including 7.3 × 10^7 for supervised training, 2.5 × 10^8 for RL, and 6.1 × 10^7 for final evaluation.The evaluation component is 16% of the total; HTPS and ABEL figures cover training only.Source: Per-Model Estimation Details · pp. 16–17

G LeanTree Comparison to Existing Tools

LeanTree is compared with existing Lean interaction and data-extraction tools, with differences in proof-state factorization, tactic handling, project context, and availability. Its Lean 4 implementation distinguishes it from the limited Lean 3 Evariste tool.

Evariste

  • Evariste supports factorized goals and detects metavariable coupling, but its dataset is unreleased and its tool is available only in a limited, nonexecutable format.Its core implementation in C++ binds to Lean 3 internals, making migration to Lean 4 difficult.Source: G LeanTree Comparison to Existing Tools · p. 17
  • LeanTree’s core logic is implemented in Lean 4 and builds on the semi-official Lean REPL, while Evariste was implemented only for deprecated Lean 3.LeanTree is consequently positioned to benefit from future community improvements to the REPL project.Source: G LeanTree Comparison to Existing Tools · p. 17

LeanDojo

  • LeanDojo provides interaction and supervised extraction for Lean 3 and Lean 4, but lacks proof-state factorization, tactic simplification, and proof-tree building.Its tactics remain in source AST form; users must choose between filtering complex tactics and retaining them with greater modeling difficulty and lower search granularity.Source: G LeanTree Comparison to Existing Tools · p. 17

Pantograph

  • Pantograph supports factorized goals and identifies metavariable coupling, but its extraction lacks tactic simplification and proof-tree construction, and it omits sub-proof size and depth.Its API treats theorems as independent units rather than gradually building a Lean context in which declarations can depend on earlier ones.Source: G LeanTree Comparison to Existing Tools · p. 17

H Dataset Schema

LeanTree samples represent Lean files and preserve proof structure along with surrounding context. The dataset schema depicts this organization.

Dataset Schema

  • Each LeanTree sample corresponds to a Lean file, preserving the project structure needed when proofs depend on earlier definitions in that file.A file contains a list of theorems, and each theorem may have multiple tactic proofs when its term contains multiple non-nested by-blocks.Source: H Dataset Schema · p. 17
  • Each tactic proof is represented as a tree whose nodes are factorized proof states and whose edges are tactic applications.Each proof node also stores its subtree size and depth.Source: H Dataset Schema · p. 17
  • The dataset records imported modules, open namespaces, and character offsets locating each theorem, proof, and tactic execution in the repository.Figure 9 presents the JSON schema of a sample.Source: H Dataset Schema · p. 17, Figure 9 · p. 18
Loading 2610.11605v1…