发布 Vampire-Hammer：用 Vampire 为 Lean 重建证明
热点事件持续更新
发布 Vampire-Hammer：用 Vampire 为 Lean 重建证明
1 篇报道1 个报道来源3 小时前更新
先了解这件事
AI 综述
Jonas Bodingbauer 与 Laura Kovács 在 arXiv 发布论文，介绍 Vampire-Hammer 工具：它调用 Vampire 自动定理证明器来证明 Lean 定理证明器中的目标，并重建经 Lean 内核检查的证明。 据论文描述，在 10 秒预算下对 196,083 个符合条件的 Mathlib 定理进行测试，Vampire-Hammer 解决了 21,158 个其他受评估工具在同样预算下未能解决的问题。
AI 根据报道生成 · 43 分钟前更新
最新进展10月31日 12:00
Vampire-Hammer：用 Vampire 自动定理证明器为 Lean 重建证明报道时间线
沿着报道，了解事件的不同侧面。
10月31日
- arXiv cs.AIVampire-Hammer：用 Vampire 自动定理证明器为 Lean 重建证明
研究者提出 Vampire-Hammer，一种面向 Lean 交互式定理证明器的工具，调用 Vampire 自动定理证明器来证明目标，并重建经 Lean 内核检查的证明。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。