NanoProof improves theorem proving efficiently in open source
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
Machine LearningArtificial Intelligence
Summary
Automated theorem proving involves using computers to check or find mathematical proofs, which can be very complex and computationally expensive. The authors introduce NanoProof, a new tool built in the Lean 4 system that can automatically prove theorems using much less computing power than similar tools. They also provide all the data and methods needed to replicate their work openly. This makes it easier for others to train and improve theorem proving systems using practical resources.
What this means in practice
- •For software developers: Integrate efficient automated theorem proving in software verification pipelines using openly available Lean 4 tools and datasets.
- •For formal methods engineers: Use NanoProof to accelerate proof discovery in formal verification projects while reducing computational resources needed.
Authors
Matěj Kripner, Milan Straka
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.