Benchmark · math
PutnamBench
PutnamBench 是一个基于大学生竞赛数学的形式化定理证明基准：它衡量一个系统能在证明助手（Lean 4、Isabelle 或 Coq）中证明多少道 Putnam 竞赛题，评分为机器验证通过的证明的数量或比例。
了解更多
- 示例
- 一道高难度的大学生 Putnam 题目——例如一个数论整除性命题、一个积分或不等式的界，或一个组合恒等式——以形式化定理陈述的形式给出，其证明留作 `sorry`，由系统补全。
- 评分方式
- 指标是系统给出完整形式化证明的题目数量（或百分比）。只有当证明助手完全验证通过时，该题才计入；部分论证或非形式化推理得零分。
- 验证方式
- 只有当目标证明助手的内核对整个证明完成类型检查、且没有 `sorry`、没有额外公理、也没有改动给定陈述时，结果才被接受——验证器的「是/否」是唯一的裁判。
- 为何重要
- Putnam 题目属于最难的大学生数学，而机器验证的证明不给错误或「奖励作弊」式推理留任何余地，这使 PutnamBench 成为 MiniF2F 之后一个更严格、难度高得多的自动定理证明与数学推理基准。
示例解析
任务
（示意性、简化。）一个 PutnamBench 格式的 Lean 4 定理，需在不使用
sorry 的情况下证明：
```lean
theorem putnam_illustrative (n : ℕ) :
∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
sorry
```解答
```lean
theorem putnam_illustrative (n : ℕ) :
∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
induction n with
| zero => simp
| succ k ih => rw [Finset.sum_range_succ, ih]; ring
```解析
前 n 个奇数之和等于 n^2；用归纳法证明：基例归约为 0 = 0，归纳步骤使用
Finset.sum_range_succ，应用归纳假设，并用 ring 收尾 k^2 + (2k+1) = (k+1)^2。它能通过仅仅是因为 Lean 内核接受每一步——真正的 PutnamBench 题目要难得多。| 日期 | 模型 | 得分 | 来源 |
|---|---|---|---|
| 2026-07-03 | Leanstral 1.5 | 587.0pts | Mistral 发布了 Leanstral-1.5-119B-A6B |
| 2026-07-03 | Leanstral 1.5 | 587.0pts | Leanstral 1.5：人人皆可拥有的丰富证明 |