NanoProof开源Lean 4定理证明器，自测MiniF2F得分50.8%

NanoProof发布了首个完全开源的Lean 4因子化执行引导定理证明器，其训练数据、提取工具、训练流程和权重均已公开。

此前该领域的先进系统多依赖大规模预训练语言模型微调，且不公开训练细节，导致研究难以复现或对比。NanoProof旨在通过计算效率支持可持续研究，使资源有限的团队也能从头构建此类系统。

作者自测显示，NanoProof在MiniF2F-Test基准上达到50.8%的pass@16准确率，比同类系统HyperTree Proof Search和ABEL分别少用约90倍和7倍的算力，比AlphaProof少用四个数量级以上的算力。

该结果来自论文作者自报，尚未经过第三方独立复现验证。代码和数据已发布于GitHub仓库kripner/nanoproof。