主要证据
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical CompetitionS1 · 主要研究来源 · 论文 · 2024-07-15
- PutnamBench formal benchmark repositoryS1 · 主要研究来源 · 代码仓库
PutnamBench 将形式定理证明评测提升到 Putnam 级本科数学
初始神经与符号证明器只能解决极少数题目，使该集合成为高难度形式推理目标。
发生了什么？
PutnamBench 发布 640 道 Putnam 定理的 1,692 个手工形式化版本，覆盖 Lean 4、Isabelle，并包含相当规模的 Coq 子集。
为什么重要？
它把形式定理证明评测从高中奥赛进一步推进到覆盖广泛的高阶本科数学。
重要性说明：PutnamBench 基于北美顶尖本科数学竞赛构建高难度多形式系统基准，并揭示当时证明器与高水平本科数学之间的巨大能力差距。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 自动定理证明器在形式化 Putnam 问题上接受评测。
- 人类贡献
- 研究者在多个证明助手中手工形式化竞赛题并构建基准。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- putnambench, lean, isabelle, coq
- 机构
- university-of-texas-at-austin
- 数学问题
- putnam-competition
- 方法
- benchmarking, formalization
全部来源与工件
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical CompetitionS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- PutnamBench formal benchmark repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2024-07-15 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。