2020年国际数学奥林匹克竞赛成绩公布，中国队获得5金1银。这是中国队在2019年与美国队并列第一后第一次获得总分。但是，在接下来的比赛中，可能会有AI球员上场破坏比赛。

图片来源:Maria Nguyen

|

quanta杂志

9月27日，第61届国际数学奥林匹克(IMO)最终结果通过官网公布。中国队的六名队员在这场比赛中获得了一枚硬件银牌，并以215分的总分获得了第一名。其中，重庆巴蜀中学的李进民得了42分，成为本次比赛中唯一的满分选手。俄罗斯队和美国队分别以185分和183分排名第二和第三；第四至第十名分别是:韩国、泰国、意大利(并列第六)、波兰(并列第六)、澳大利亚、英国、巴西。

这个IMO

可能很快就会成为历史记忆中的游戏。原因有二:一是受新冠肺炎疫情影响，比赛首次远程在线举行；其次，很有可能这将是数学天才们最后一次不受AI“干扰”的比赛。

是的，计算机研究人员把IMO视为证明机器可以被设计成像人类一样思考的理想场所。如果一个AI系统能够赢得竞争，就意味着它已经能够在人类认知的一个重要维度上与它的创造者竞争。

AI能否成为IMO冠军？

微软研究团队的丹尼尔·塞尔萨莫(Daniel Selsamo)说:“对我来说，IMO代表了聪明人在训练后能解决的最困难的问题。”。他是国际海事组织大挑战的创始人之一。该项目旨在训练一个人工智能系统，以在世界顶级数学竞赛中赢得金牌。

自1959年以来，IMO汇集了世界各地数学最好的高中生。在为期两天的比赛中，参与者每天有四个半小时的时间回答三个日益困难的问题，每题满分为7分。就像奥运会一样，总分最高的一方获得金牌。IMO顶尖选手往往开启“数学传奇之路”。他们中的许多人选择在这个领域继续深造，成为数学方面的顶尖学者。

例如，玛丽亚姆·米尔扎哈尼曾在1994年和1995年两次获得国际海事组织的金牌，后来成为斯坦福大学的数学教授。2014年37岁时，她因在黎曼曲面及其模态之间的动力学和几何方面的杰出研究空(编者注:20)获得了被称为诺贝尔数学奖的菲尔兹奖(Fields Prize)，这是最近的菲尔兹奖(2018)的获得者之一，德国数学家彼得·斯科尔斯(Peter Scholze):他从2004年到2007年连续参加了四届IMO会议，并获得了三枚金牌。代数几何是他的主要方向之一，获得了许多学术荣誉和重要奖项。年轻的中国数学家云志伟是2000年国际数学家大会的金牌获得者。他目前是美国麻省理工学院的数学教授。他因在表象理论、代数几何和数论方面的基本贡献获得了拉玛努金奖和新视野奖。。。。。。

从左到右分别是玛丽雅姆·米尔扎哈尼、彼得·舒尔茨和云之维

但是，IMO与学术研究完全不同。就数学知识的存储而言，IMO的问题很简单，因为不要求回答者掌握高等数学，甚至连微积分都被认为超出了竞赛范围。然而，它们也极其困难。以1987年在古巴举行的第五届国际海事组织竞赛为例:

n是大于或等于3的整数。请证明平面上有一个n点的集合，这样任意两点之间的距离是无理数，每三点形成一个有理数面积的非退化三角形。

和很多IMO的问题一样，这个问题乍一看似乎是不可能的。

“读完标题，你会觉得‘我做不到’，”来自伦敦帝国理工学院的凯文·巴扎尔回忆道，他是“国际海事组织挑战”小组的成员，并在1987年获得了国际海事组织的金牌。“对年轻学生来说，这是极其困难的问题。他们只有把自己知道的所有想法巧妙地结合起来，才能做出这些问题。”

回答IMO的问题往往需要灵光一现，而这短暂的第一步对于目前的AI系统来说是极其困难的。

举例说明。数学中最古老的定理之一就是欧几里德证明了公元前300年就有无穷多个素数。最开始欧几里德发现，把所有已知的素数相乘加一，总能得到一个新的素数。虽然下面的证明过程很简单，但是这种开放的思想在刚出现的时候确实是一门艺术。

“你不能让电脑想出那个主意，”Buzzard说。至少现在还没有。

晋升之路艰难

“海事组织挑战”团队正在使用微软研究员莱昂纳多·德·莫拉在2013年发布的一个名为“精益”的项目。它是一个“证明助手”，负责检查数学家的工作，将证明过程中一些简单单调的部分自动化。

Lean的主页

德莫拉和他的同事想用Lean作为“问题解决者”，自己写IMO问题的证明过程。但目前连一些问题涉及的概念都无法理解。如果你想提高它的性能，有两件事需要改变。

第一，精益需要学习更多的数学知识。这个项目使用mathlib，一个正在开发的数学库。现在包含了一个大二数学专业的学生应该掌握的所有数学知识，但是IMO还是有一些基础知识的空白。

第二个挑战更大:教Lean如何运用所学的数学知识。在Lean之前，依靠决策树找到下一步的最佳动作，帮助其他AI在桌游等复杂的人类比赛中成功获胜。所以“IMO挑战赛”团队希望用类似的方式训练Lean，找到一种数学证明的方法。

“成千上万的解决问题的想法首先产生，然后依次被拒绝，直到系统遇到正确的一个而停止。Buzzard解释说:“如果只有这种方法能让计算机产生我们想要的聪明和优秀的解决方案，也许‘海事组织挑战’就能成为现实。”

“游手好闲”的数学思维

问题是，什么是数学思维？这个概念出奇的难解释。从较高的层面来说，数学家在解决一个新问题时会做出很多不合理的行为。

“对于许多国际海事组织的主题来说，关键的一步是‘尝试找出’主题并找到模式。”塞尔萨姆说。当然，研究人员仍然不知道如何让计算机和问题“玩游戏”。

数学证明从低级来说，本质上是一系列非常明确的逻辑步骤。IMO研究人员可以向Lean展示以前IMO认证过程的细节来培训它。但是在更小粒度的层面(意味着更详细的数据)，针对特殊问题的针对性证明会变得过于专业。

换句话说，“证明过程中没有任何东西可以用于下一个问题。”塞尔萨姆说。

为了解决这个问题，“IMO挑战赛”团队需要数学家为之前的IMO课题写一个详细的形式化证明过程。团队将继续使用这些认证流程来尝试完善背后的技能或策略。然后，他们将训练人工智能系统，在这些策略中寻找“双赢”的组合，以解决以前没有出现的海事组织问题。根据Selsam的观察，难点在于数学竞赛比最复杂的桌游难赢多了。

“也许围棋的目标是找到下棋的最佳方法，而数学的目标是首先找到最佳的游戏策略，然后找到最佳的行动计划，”他说。

图片来源:罗马尼亚-内部人士

为金牌梦想而奋斗

“海事组织大挑战”目前只是一个疯狂的想法。德莫拉说，如果莱恩参加今年的比赛，“我们可能会得0分”。

然而，研究人员希望他们能在下次比赛前努力实现几项突破。他们计划改进mathlib的知识库，以便Lean能够理解所有问题。他们也希望获得之前IMO题目的官方详细证明，为Lean提供基本的比赛脚本学习。

也许到那时奥运金牌还遥不可及，但至少Lean可以出线，站在这场智力竞赛的起跑线上。

“目前，我们已经做了很多事情，但是还没有真正值得做标记的进展，”塞尔萨姆说，而任中团队还有很长的路要走。“明年会更努力。”

也许几年后，IMO的金牌就不再属于人类了。