为什么重要
Putnam 竞赛是北美最难的大学数学竞赛，中位数得分通常为 0 分。Putnam-AXIOM 将这些难题转化为可自动验证的评测，是测量模型高阶数学推理的前沿基准。
构建方式
- 收集 1985-2023 年 Putnam 竞赛真题
- 将部分题目形式化为 Lean 4 可验证格式
- 数值答案用 SymPy 自动验证
任务示例
问题：“Prove that for every positive integer n, the number n! + 1 is not a perfect power.”
关键发现
- 所有前沿模型解题率均低于 10%
- 证明类题目比计算类更难
- 形式化验证消除了评估模糊性
关联基准
- FrontierMath：研究级数学
- AIME：数学奥赛
- FLTEval：形式化证明
不足与展望
- 题库规模有限（236 题）
- 形式化覆盖不完整
- 部分题目可能出现在训练数据中