发表机构
Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University（查理大学数学与物理学院形式与应用语言学研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
NanoProof是Lean 4中首个因子化执行引导型开放自动定理证明器，以低计算量实现优于同类系统的性能，证明该类证明器可利用适度资源从头构建。
AI 中文摘要
我们推出NanoProof，据我们所知，它是Lean 4中首个因子化执行引导型定理证明器，其训练数据、提取工具、训练流程及权重均已发布，可通过开源资源实现端到端可复现。为此，我们构建并发布了结构化证明树数据集，以及用于Lean 4形式验证器内程序化交互与数据提取的工具。为支持可持续研究，我们聚焦计算效率以实现可及的训练与评估。NanoProof在MiniF2F-Test上达到50.8%的pass@16，超过同类别最接近的两个系统HyperTree Proof Search和ABEL，计算量分别减少约90倍和7倍，且比AlphaProof少四个数量级以上。虽存在更强的开放权重证明器，但它们均基于大型预训练语言模型微调，且未发布训练数据或流程；NanoProof表明，因子化执行引导型证明器类别可利用适度资源从头构建。
英文摘要
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.
Comments18 pages, 8 figures. Code: https://github.com/kripner/nanoproof
