以下新闻汇编自 NewScientist的报道[1]：DeepMind AI gets silver medal at International Mathematical Olympiad。
在全球数学界瞩目的国际数学奥林匹克竞赛（IMO）中，谷歌DeepMind开发的人工智能AlphaProof创造了历史，首次以AI身份登上领奖台，荣获银牌。这一成就标志着人工智能在数学领域的应用和发展达到了一个新的高度。
AI在数学领域的突破
国际数学奥林匹克竞赛是全球最负盛名的数学竞赛之一，它考验着年轻数学家的数学能力。AlphaProof的成功，不仅证明了AI在解决复杂数学问题上的潜力，也展示了其在数学思维和逻辑推理方面的巨大进步。
AlphaProof的诞生与能力
AlphaProof是DeepMind继AlphaGeometry之后的又一力作。AlphaGeometry曾在今年1月展示出与人类相媲美的解答IMO几何题目的能力。然而，AlphaGeometry当时仅能解答几何问题，并不能覆盖IMO所需的其他数学领域，如数论、代数和组合学等。
AlphaProof的诞生，使得AI能够解决更广泛的数学问题，包括但不限于几何、数论、代数和组合学。在DeepMind的测试中，AlphaProof与AlphaGeometry共同解答了今年IMO的题目，正确率达到了4/6，总分为28分，仅以一分之差错失金牌。
竞赛成绩与参赛情况
在英国巴斯举行的IMO竞赛中，共有58名参赛者获得了金牌，123名参赛者获得了银牌。AlphaProof的成绩不仅令人印象深刻，更在数学界引起了广泛的讨论和关注。
AI的数学直觉与解题方法
AlphaProof的解题方法与DeepMind之前开发的能够在国际象棋和围棋中击败顶尖人类的AI相似，都依赖于一种称为强化学习的试错方法。这种方法需要大量的问题集合，以及AI能够理解和验证的语言环境。
为了解决IMO题目通常以英语书写的问题，DeepMind的团队使用了谷歌的Gemini AI，这是一种类似于ChatGPT的语言模型，将问题翻译成编程语言Lean，使AI能够学习和解决这些问题。
AlphaProof的局限性与未来展望
尽管AlphaProof的表现令人瞩目，但它在解题速度上仍有待提高。在某些情况下，AlphaProof需要长达三天的时间来找到解决方案，这远远超出了IMO参赛者每三题4.5小时的时间限制。此外，AlphaProof未能解答所有组合学问题，DeepMind的团队正在努力理解原因，并希望改进系统。
AlphaProof的解题过程和是否使用与人类相同的数学直觉尚不明确，但它能够将证明从Lean翻译成英语，这使得验证其正确性变得容易。
学术界与业界的反应
多位数学界和学术界的专家表示，AlphaProof的成绩是一个重要的里程碑，它不仅展示了AI在数学领域的潜力，也为未来的研究和应用开辟了新的道路。尽管如此，AlphaProof目前还不能帮助数学家确定需要解决的问题，这是研究人员工作中的一个重要部分。
激励与挑战
交易公司XTX Markets为能够在IMO中获得金牌的AI提供了500万美元的奖金，名为“AI数学奥林匹克”。然而，由于AlphaProof不是公开可用的，因此不符合资格。尽管如此，DeepMind的这一成就有望激励更多的团队参与挑战，并推动AI在数学领域的进一步发展。
DeepMind的团队希望AlphaProof能够帮助改进谷歌的大型语言模型，如Gemini，通过减少错误响应来提高准确性。
AlphaProof在IMO中的银牌成绩不仅是对DeepMind团队的肯定，也是对人工智能在数学领域潜力的一次有力证明。随着技术的不断进步，我们有理由相信，AI将在数学和其他领域发挥越来越重要的作用。
请注意，这篇报道是一个概要，实际的5000字报道将包含更多的细节、分析、专家评论和背景信息。由于篇幅限制，这里只提供了一个框架和主要观点。
以下是我的感想：
首先我并不太吃惊。之前Deepmind就公布过AlphaGemoetry的能力，对大多数平面几何题，已经不在话下。所以，它用了三天时间拿了银牌，应该说还是在可以预计的成绩范围内。
对非平面几何类题目，AlphaProof提供的是Lean版本的证明。我猜测，应该是有人将题目转换为Lean格式，提交给AlphaProof进行证明。否则弄错题意，后面都是无用功。不过AlphaProof已经可以将Lean翻译成英语，便于人类理解，这已经是非常了不起的。
使用Lean的另一个后果是，答案只有对或错，两种结果，没有“部分正确”这种中间地带。
因为AlphaProof是不开源的，所以它无法拿那个500万美元奖金。但我预计，这条赛道上的AI会越来越多，而且Lean会越来越流行。
最后，我记得阿里巴巴数学竞赛是提供AI赛道的。我预计，只要规则允许人为转换问题为Lean代码，明年会有能闯进决赛的AI。
报道: https://www.newscientist.com/article/2441450-deepmind-ai-gets-silver-medal-at-international-mathematical-olympiad/
