正文：谷歌DeepMind团队在Nature上公开了其IMO金牌模型AlphaProof的技术细节。核心团队仅10人，开发历时一年，生成8000万道数学题用于AI训练。AlphaProof基于Lean定理证明器构建强化学习环境，将数学证明过程转化为游戏关卡，使用30亿参数的Transformer模型作为核心，并结合改进的树搜索算法。2024年IMO比赛中，AlphaProof成功解决三道难题（包括最难的P6），最终夺得金牌。系统通过测试时强化学习生成变体问题并进行针对性训练，展现了强大的解题能力。尽管依赖Lean定理证明器且在处理全新定义时存在局限性，但其反证功能和形式化能力受到数学家高度评价。谷歌已开放AlphaProof供科研使用。