arXiv：cs.AI· Mat\v{e}j Kripner, Milan Straka·· 3 小时前
NanoProof：在 Lean 4 中实现开放高效的自动定理证明
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
AI 导读
NanoProof 是首个训练数据、提取工具、训练流程与权重全部开源的 Lean 4 因子化执行引导定理证明器，可端到端复现，并附带结构化证明树数据集与 Lean 4 数据提取工具。它在 MiniF2F-Test 上实现 50.8% pass@16，算力消耗约为 HyperTree Proof Search 的 1/90、ABEL 的 1/7，比 AlphaProof 少四个数量级以上。
正文
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.
| Comments: | 18 pages, 8 figures. Code: this https URL |
| Subjects: | Machine Learning (cs.LG); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.11605 [cs.LG] |
| (or arXiv:2610.11605v1 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2610.11605 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Matěj Kripner [view email]
[v1]
Thu, 8 Oct 2026 09:49:39 UTC (486 KB)
来源：arXiv：cs.AI · arxiv.org