cs.LGOct 8, 2026

NanoProof: Open and Efficient Automated Theorem Proving in Lean 4

Authors: Matěj Kripner, Milan Straka

Organizations: Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University Prague, Czech Republic

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

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 .
Figure 2
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.
Figure 4
Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

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.
CategoryHyperparameterValue
Prover NetworkTotal Parameters1B
Number of Blocks26
dmodeld_{model}1664
Attention Heads13
Feed Forward Widening Factor4
Vocabulary Size50,44150{,}441
Appendix
Table 1. Architectural, optimization and search hyperparameters.
Figure 7. Example Lean theorem and its corresponding executable proof tree extracted using LeanTree. Some tactics and hypotheses are omitted.
Figure 8. Example Lean theorem and its corresponding executable proof tree extracted using LeanTree. Some tactics and hypotheses are omitted.

Explore similar work

CardsList

  1. Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

    Jun 10, 2026Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5Automated Theorem ProvingEfficient Language Model Training

    Imperial College London · University of Edinburgh · Nanyang Technological University +1

  2. MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

    May 26, 2026Jinzheng Li, Zeru Zhu, Yuanjie RenAutomated Theorem ProvingLean Theorem Proving

    1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

  3. Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

    Jun 4, 2026Jui-Hui Chung, Ziyang Cai, Zihao Li +14Automated Theorem ProvingLean Theorem Proving

    1Princeton Language and Intelligence, Princeton University · 2Amazon.