NanoProof：开源可复现的Lean 4定理证明器
热点事件持续更新
NanoProof：开源可复现的Lean 4定理证明器
1 篇报道1 个报道来源2 小时前更新
先了解这件事
AI 综述
研究者 Matěj Kripner 与 Milan Straka 发布 NanoProof，称这是首个训练数据、提取工具、训练流程与权重全部开源的 Lean 4 因子化执行引导定理证明器，可端到端复现，并附带结构化证明树数据集与数据提取工具。 在 MiniF2F-Test 基准上，NanoProof 实现 50.8% pass@16，算力消耗约为 HyperTree Proof Search 的 1/90、ABEL 的 1/7，比 AlphaProof 少四个数量级以上。上述性能与开源范围均出自发布者本人的介绍。
AI 根据报道生成 · 2 小时前更新
最新进展10月9日 12:00
NanoProof：在 Lean 4 中实现开放高效的自动定理证明报道时间线
沿着报道，了解事件的不同侧面。
10月9日
- arXiv：cs.AINanoProof：在 Lean 4 中实现开放高效的自动定理证明
NanoProof 是首个训练数据、提取工具、训练流程与权重全部开源的 Lean 4 因子化执行引导定理证明器，可端到端复现，并附带结构化证明树数据集与 Lean 4 数据提取工具。它在 MiniF2F-Test 上实现 50.8% pass@16，算力消耗约为 HyperTree Proof Search 的 1/90、ABEL 的 1/7，比 AlphaProof 少四个数量级以上。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。