为什么重要
Putnam 竞赛是北美最难的大学生数学竞赛之一，中位数得分常年接近 0。把它的真题形式化，等于给「AI 做数学」设了一条远离刷分污染的标尺——这些题不在常规预训练语料的常见题堆里，而且答案必须由证明助手校验，编不出来就是编不出来。
它的第二个价值是跨证明助手。同一道题分别给 Lean 4、Isabelle、Coq 三种陈述，可以直接比较「模型在哪种形式化语言上更强」。这个维度此前没有基准覆盖：miniF2F 只有 Lean/Isabelle 子集，ProofNet 主要面向 Lean。
对数据侧的启示：形式化数学数据的稀缺性是硬瓶颈。Lean 的 mathlib 规模远小于自然语言数学语料，而 Putnam 这类竞赛题的形式化又要靠人工翻译，成本极高。谁能在「自动形式化」上做出突破，谁就能实质扩大这块训练数据的供给。
构建方式
- 收集 1962 年以来历届 Putnam 竞赛的题目（含 A/B 两部分）
- 人工把每题翻译成三种形式化陈述：Lean 4（基于 mathlib）、Isabelle（基于 Isabelle/HOL 库）、Coq（基于 Coq 标准库）
- 对可获取官方解答的题目，附带自然语言参考答案
- 评测时把模型生成的证明喂给对应证明助手，编译/校验通过才算成功，不做近似判断
- 部分子集额外提供「已知解答题」与「待证明题」的区分
任务示例
自然语言原题（Putnam 1995 A1 风格）：
设 S 是平面上到四边形四顶点距离之和最小的点，证明……
Lean 4 形式化陈述（示意）：
theorem putnam_1995_a1
(A B C D : EuclideanSpace ℝ (Fin 2))
(h : Convex ℝ (convexHull ℝ {A, B, C, D})) :
∃ S ∈ convexHull ℝ {A, B, C, D},
∀ P ∈ convexHull ℝ {A, B, C, D},
dist P A + dist P B + dist P C + dist P D ≥
dist S A + dist S B + dist S C + dist S D := by
-- 模型需要在这里给出证明模型输出必须让 Lean 编译器接受，任何一处类型错误或逻辑跳跃都会失败。
最新进展
- 发布时的基线显示：即便是最强的通用模型，解题率也只在个位数百分比，远低于人类选手中的优秀者
- 此后专用定理证明模型（各类 Lean 证明器）把成绩往上推，但整体仍属未饱和区间
- 围绕它衍生出一批「自动形式化」工作：把自然语言数学题自动转成 Lean 陈述，缓解数据稀缺
关键发现
- 形式化是一道硬门槛：自然语言能讲清楚的数学思路，写进 Lean 里往往卡在类型与库调用
- 三种语言难度不同：同一模型在 Lean / Isabelle / Coq 上的表现差异明显，反映训练语料分布不均
- 难以污染：竞赛真题 + 机器校验，使得「背答案」这条路基本走不通
- 数据瓶颈在自动形式化：人工翻译成本决定了这类基准的规模上限，也决定了形式化训练数据的供给上限