NanoProof Releases Open-Source Lean 4 Theorem Prover, Self-Reports 50.8% Score on MiniF2F
First fully open factorized execution-guided Lean 4 theorem prover released, significantly reducing compute requirements.
중요도중대증거E2 미복제작성 방식간략
NanoProof has released the first fully open-source factorized execution-guided theorem prover for Lean 4, making its training data, extraction tools, training pipeline, and weights publicly available.
Previous advanced systems in this field often relied on fine-tuning large pretrained language models without releasing training details, hindering reproducibility and comparison. NanoProof focuses on compute efficiency to support sustainable research, allowing teams with modest resources to rebuild such systems from scratch.
The authors self-report that NanoProof achieves 50.8% pass@16 accuracy on the MiniF2F-Test benchmark, using approximately 90x and 7x less compute than similar systems HyperTree Proof Search and ABEL, respectively, and more than four orders of magnitude less compute than AlphaProof.
These results are self-reported by the paper's authors and have not yet been independently reproduced. Code and data are available in the GitHub repository kripner/nanoproof.