NanoProof：Lean 4 中开放且高效的自动定理证明

我们介绍了 NanoProof，据我们所知，这是 Lean 4 中首个因子化执行引导定理证明器，其训练数据、提取工具链、训练流程和权重均已发布，因此可以完全使用开源资源实现端到端复现。为此，我们构建并发布了一个结构化证明树数据集，以及一个用于在 Lean 4 形式化验证器中进行程序化交互和数据提取的工具。为支持可持续研究，我们注重计算效率，以促进易于获取的训练与评估。在 MiniF2F-Test 上，NanoProof 的 pass@16 达到 50.8%，超过了同类中最接近的两个系统 HyperTree Proof Search 和 ABEL，而所需计算量约分别少 90 倍和 7 倍；与 AlphaProof 相比，所需计算量则少四个数量级以上。虽然存在更强的开放权重证明器，但它们都是基于大型预训练语言模型进行微调的，既不发布训练数据，也不发布训练流程；NanoProof 表明，因子化执行引导类证明器可以使用适度资源从头重建。