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

2025年8月，字节发布全新数学模型Seed-Prover，在复杂数学问题解决领域取得突破性进展。该模型基于Lean 4形式化推理框架，并创新采用引理式证明范式，模块化处理数学推理过程。其在MiniF2F数据集上实现100%正确率，解决了78.1%的历年IMO难题，并在普特南数学竞赛中表现优异。此外，Seed-Prover集成专用几何推理引擎Seed-Geometry，在IMO 2025比赛中达到银牌水准，完整解决6道题中的4道及部分证明。Seed-Geometry还在2秒内解出IMO 2025第2题，展现了卓越效率和泛化能力。前谷歌成员Deedy Das评价称，字节是唯一一家为IMO发表完整论文的AI实验室。

2025年7月，IMO赛场上演AI巅峰对决。7月19日，顶尖大模型几乎全军覆没；两天后，OpenAI和DeepMind等实验室斩获5/6题。7月23日，哈佛与UCLA学生用Gemini 2.5 Pro+多轮验证框架发布论文并开源代码。次日，蚂蚁AWorld团队仅用6小时复现DeepMind成果，开源一键运行的多智能体IMO系统。实验表明，多智能体协同能超越单模能力，解决复杂IMO问题，并提出构建最优输入、实现元认知等理论支持。AWorld采用事件驱动架构，具备模型即插即用、全链路可观测性等优势。团队透露，未来将测试“多智能体+形式化验证”组合，目标直指Lean4形式化证明。IMO或成人类最后一次战胜AI的机会。

标题：DeepSeek加持，北大几何模型达IMO金牌水平！32个CPU核心和1块4090就能实现满血解题 国产AI几何模型TongGeometry性能达IMO金牌水平，媲美谷歌DeepMind的AlphaGeometry。TongGeometry使用策略网络和价值网络，源自微调版DeepSeek-C...

Google DeepMind团队开发的AlphaGeometry2系统在国际数学奥林匹克竞赛(IMO)中解决了84%的几何难题，首次超过IMO平均金牌得主的表现。AlphaGeometry2是一个神经-符号混合系统，基于Gemini语言模型，并在大量合成数据上训练。相比前代AlphaGeometry，其求解速度提高了300倍，并能处理更复杂的几何问题。尽管如此，AlphaGeometry2仍存在局限性，未能解决涉及变量点个数、不等式及非线性方程的题目。伦敦帝国理工学院数学家Kevin Buzzard认为计算机有望在IMO竞赛中拿满分。相关研究论文已发布在arXiv上。

Google DeepMind团队开发的AlphaGeometry2系统在解决国际数学奥林匹克（IMO）几何难题方面取得了突破。该系统解决了84%的几何难题，首次超过IMO平均金牌得主的水平。AlphaGeometry2是一个神经符号混合系统，基于Gemini语言模型，能处理更复杂的几何问题，包括物...