Rust-Prover 用 Lean 4 验证器完成 VeriContest 全部证明
热点事件观察中
Rust-Prover 用 Lean 4 验证器完成 VeriContest 全部证明
1 篇报道1 个报道来源1 天前更新
先了解这件事
AI 综述
Traian Serbanuta 等作者发表论文，报告用 Rust-Prover（以 Lean 4 作为最终检查的 Rust 验证器）解决了 VeriContest 证明生成任务：1007 道题的全部 1325 个定理均被证明。 其中 1259 个定理在 Claude Opus 5.5 上单次运行不到 32 小时内完成，中位耗时 3.2 分钟、每个证明 1.17 美元，70% 一次通过。作者还称，最便宜的 Claude 配置 Sonnet 5.5 在低努力下证明了全部 50 个最难的定理，而 Opus 5.5 单独运行未能证明其中一个。
AI 根据报道生成 · 1 天前更新
最新进展10月12日 12:00
用 Lean 4 验证器 Rust-Prover 攻克 VeriContest 证明生成任务报道时间线
沿着报道，了解事件的不同侧面。
10月12日
- arXiv cs.AI用 Lean 4 验证器 Rust-Prover 攻克 VeriContest 证明生成任务
Rust-Prover 用 Lean 4 作为最终检查，完成了 VeriContest 全部 1007 道题、共 1325 个定理的证明，其中 1259 个在 Claude Opus 5.5 上单次运行不到 32 小时内完成，中位耗时 3.2 分钟、每个证明 $1.17，70% 一次通过。
本事件热度走势
- 可比范围当前
- 4
- 可比范围峰值
- 1010月12日 13:00
- 近 24 小时变化
- -51%
02.557.510
18:0010月13日06:0012:00
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。