NanoProof：全开源的 Lean 4 自动定理证明器
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
一个从数据、工具到权重全开源的 Lean 4 定理证明器，用 AlphaProof 万分之一不到的算力拿到 MiniF2F 50.8% pass@16，搞形式化验证的可以自己复现了。
NanoProof 是首个端到端开源的 Lean 4 因子化执行引导定理证明器，发布了结构化证明树数据集、交互与数据抽取工具、训练流程和权重。它在 MiniF2F-Test 上取得 50.8% pass@16，超过同类的 HyperTree Proof Search 和 ABEL，所用算力分别少约 90 倍和 7 倍。相比 AlphaProof，其算力消耗少四个数量级以上。论文证明这类证明器可以在 modest 资源下从零重建，而不依赖大型预训练模型的微调。
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
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.
