核心观点 - 谷歌DeepMind研发的AI系统AlphaProof在国际数学奥林匹克竞赛（IMO）中取得28分（满分42分），达到银牌水平，距离金牌线仅差1分，这是AI首次在此类顶级数学赛事中获得奖牌级成绩 [3][4][18] 技术方法 - AlphaProof结合了预训练大语言模型的直觉和AlphaZero强化学习算法的探索能力，其核心是将AI思维“硬化”成可被计算机逐行检验的形式化证明语言Lean [8][6][7] - 系统首先利用谷歌Gemini模型将近一百万道自然语言数学题翻译成Lean代码，构建了约8000万条形式化数学命题的题库供AI练习 [10] - 训练过程分为两步：先通过监督学习微调掌握基本证明技巧，再进入强化学习阶段，通过类似AlphaGo的自我对弈在数百万次问题证明中不断进步 [10] - 在解题搜索中采用类似蒙特卡罗树搜索的策略，智能拆解复杂问题为子目标，避免了暴力穷举 [11][16][17] 竞赛表现 - AlphaProof与专攻几何的AlphaGeometry 2联手，在2024年IMO的6道题中解出4道，获得28分，处于银牌段顶端 [18] - AlphaProof单独解决了3题（包括2道代数题和1道数论题），其中整场最难的第6题在600多名顶尖学生中仅5人满分解决 [18] - 剩余1道几何题由AlphaGeometry 2完成，而两道组合数学题因难以形式化和搜索爆炸等原因未能攻克 [18] 当前局限 - 解题效率较低：人类选手需在4.5小时内完成3题，而AlphaProof解决3题耗费了将近3天时间 [21] - 通用性不足：未能解决两道组合数学题，这类高度非结构化创新思维的问题仍对AI构成挑战 [21] - 无法自主读题：需要人工先将题目翻译成Lean形式化表达，不具备自然语言理解能力 [21] 未来方向 - 研发方向包括让AI直接阅读理解自然语言表述的数学题，并给出形式化证明 [23] - 针对不同类别数学问题（如组合数学或几何）引入更专业策略，如融合符号计算、知识库或分领域训练模型 [24] - 未来可能实现数学家与AI证明助手协同工作，AI负责快速验证猜想和尝试思路，人类专注于提出问题和宏观构想 [24] - 其形式化推理能力对AI安全和可靠性有启发意义，输出的每一步推理可追溯、验证，有助于减少大模型的荒诞臆测 [25]