Putnam

自1938年起，威廉·洛厄尔·普特南数学竞赛（Putnam）以其高难度和低得分率闻名，近年成为检验大语言模型（LLM）数学推理能力的标杆。近期，Google DeepMind推出LEAP框架，显著提升了通用LLM在形式化数学证明中的表现。该框架通过“学习-精炼”循环，使模型在12道Putnam 2025题目上成功证明全部题目，并在Lean-IMO-Bench上达到70%成功率，较基线提升约60个百分点。同时，Goedel-Architect项目提出蓝图生成与精炼方法，进一步推动了形式化定理证明的自动化。这些进展表明，将LLM与交互式定理证明器（如Lean）结合，能有效处理竞赛级数学问题。当前焦点在于方法的泛化性：LEAP对特定题目集的高性能是否能迁移至更广泛的数学领域？未来观察点包括：新技术是否会在明年的Putnam竞赛中公开测试，以及这类工具对数学教育或研究的实际影响。尽管提升显著，但模型仍依赖大量时，且面对未见过题型时的稳定性待考。