arXiv · cs.AI· Matěj Kripner·· 18 天前精选AI 评分52
NanoProof 论文提出端到端可复现的 Lean 4 自动定理证明器
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
来源与原文
arXiv · cs.AI
作者：Matěj Kripner
发布时间：（北京时间）
阅读原始来源 · arxiv.org ↗完整链接与内容说明
https://arxiv.org/abs/2610.11605v1
本站目前仅有 AI 导读与摘要，未展示原文正文；技术细节、代码和完整结论请查看原始来源。
AI 导读
Matěj Kripner 发布 NanoProof，据作者所知是首个训练数据、提取工具、训练管线和权重全部开源的因子化执行引导式 Lean 4 定理证明器。该方法在 MiniF2F-Test 上取得 50.8% pass@16，算力约为 HyperTree Proof Search 的 1/90、ABEL 的 1/7，比 AlphaProof 少四个数量级以上；论文同时发布了结构化证明树数据集和 Lean 4 程序化交互与数据提取工具。原文链接 https://arxiv.org/abs/2610.11605v1。
推荐理由
论文公开了训练数据、提取工具、训练管线和权重，读者可以低成本复现这一类 Lean 4 定理证明器并对比算力开销。
来源：arXiv · cs.AI · arxiv.org