NanoProof：首个Lean 4端到端复现定理证明器

发生了什么

据arXiv cs.LG论文，研究者推出NanoProof，这是首个在Lean 4中实现端到端复现的因子化执行引导定理证明器，其训练数据、工具、管道和权重均已开源。该模型在MiniF2F-Test上达到50.8% pass@16准确率，计算资源消耗比同类系统少约90倍至7倍，比AlphaProof少四个数量级以上。研究证明该类证明器可用适度资源从头重建。