图片来源：pixabay
今年，可能是最后一届“纯人类”参赛的IMO （国际奥数竞赛）。因为在明年，AI可能也会加入这场金牌争夺战中，成为一名“种子选手”。
9 月 27 日，第 61 届国际数学奥林匹克竞赛（International Mathematical Olympiad, IMO）通过官网公布了比赛的最终成绩。中国队的 6 名选手在本次比赛中摘取五金一银，以 215 分获得总成绩第一。其中，来自重庆市巴蜀中学校的李金珉获得 42 分，成为本届比赛唯一满分选手。俄罗斯队和美国队分别以 185 分和 183 分位列第二、三名；而第四到十名依次为：韩国、泰国、意大利（并列第 6）、波兰（并列第 6）、澳大利亚、英国、巴西。
图片来源：官网截图
这届 IMO 或许即将成为一场被历史铭记的比赛。原因有二：首先，在新冠疫情影响下，竞赛首次在线上远程举行；其次，这很有可能是参赛的数学天才们不被人工智能（AI）“打扰”的最后一届比赛。
计算机研究人员把 IMO 看作是可以证明机器能被设计成像人一样思考的理想之地。如果一个 AI 系统可以赢得竞赛，那就说明它在人类认知层面的某个重要维度已经可以和它的创造者相匹敌了。
IMO赛事究竟多厉害
自 1959 年起，IMO 就集结了全世界最擅长数学的高中生。在两天的比赛期间，参赛者每天有四个半小时来回答 3 个难度逐渐增加的问题，每道题满分为 7 分。就像奥林匹克运动会一样，总分名列前茅者获得金牌。名列前茅的 IMO 参赛者经常由此开启"数学界的传奇之路”。他们中的很多人选择在这个领域继续深造，变成了研究数学的顶尖学者。
比如 1994、1995 年连续两次获得 IMO 金牌的玛丽亚姆·米尔扎哈尼（Maryam Mirzakhani），后来成为了斯坦福大学数学教授，并且在 2014 年 37 岁时因为对黎曼曲面和及其模空间的动力学和几何学的突出研究，获得了有“数学界诺贝尔奖”之称的菲尔兹奖（编者注：2017 年米尔扎哈尼因乳腺癌去世，享年 40 岁）。还有最近一届（2018 年）的菲尔兹奖得主之一、德国数学家彼得·舒尔茨（Peter Scholze）：他曾在 2004~2007 年连续参加 4 届 IMO 并获得 3 块金牌，代数几何领域是其主攻方向之一，目前已经拿下了多项学术荣誉和重要奖项。中国青年数学家恽之玮是 2000 年 IMO 的金牌得主，目前在美国麻省理工学院任数学系教授，因在“表示论，代数几何和数论等方向诸多基本性的贡献”获得过拉马努金奖和科学突破奖新视野奖......
“于我而言，IMO 代表了聪明人在经过训练后能够解决的、最难的一类问题，”微软研究团队的 Daniel Selsamo 说道。他是“ IMO 大挑战”（IMO Grand Challenge）的创始人之一。该项目旨在训练一个 AI 系统在世界顶级数学竞赛中获得金牌。
AI选手身份大揭秘
这名潜入IMO赛事的AI名为Lean，由微软的研究人员开发。
微软的研究人员从2013年开始研发Lean，希望让AI能拥有自主判断、根据假设进行演绎的能力。
也就是说，它是个旨在缩小交互式定理证明、与自动定理证明之间的差距的开源项目。
自动定理证明：对数学中提出的定理或猜想，寻找一种证明或反证的方法。系统不仅能根据假设进行演绎，还要有一定的判定技巧。
交互式定理证明：借助计算机辅助证明工具，理解检验数学定理正确性，完成数学定理的证明。
Lean已经推出了3个版本，现在的第四个版本Lean 4还在完善中，现在的逻辑系统基于依赖类型理论，已经强大到足以证明所有的常规数学定理。
也就是说，想要让它自己证明IMO中提出来的、此前“没见过的”数学问题，依旧非常困难。
目前，Lean 4还没有彻底做好准备，作者Leonardo de Moura表示，如果让它参加今年的IMO，“可能只能得0分”。
AI如何解答数学题
IMO 和学术研究完全不同。从对数学知识的储备来讲，IMO 的问题是简单的，因为它们不要求答题者掌握高等数学，即便是微积分都被认为超出了竞赛范围。然而，它们同时又极难。以 1987 年在古巴举行的 IMO 竞赛中的第 5 题为例：
n 是大于或等于 3 的整数。请证明平面上存在这样一个含有 n 个点的集合，使任意两点的距离为无理数且每 3 个点构成一个面积为有理数的非退化（三点不共线的）三角形。
和很多 IMO 的题目一样，初看这道题似乎不可能成立。
“你阅读完题干后会觉得‘我做不出来’，”来自伦敦帝国理工学院的 Kevin Buzzard 回忆道，他是“IMO 大挑战”团队的一员，曾获得过 1987 年 IMO 的金牌。“它们对年轻学生来讲是极难的问题，他们只有将自己知道的所有想法巧妙地结合起来才有可能做出这些题。”
解答 IMO 的问题常常需要“灵光一现”，而这个短暂的第一步对目前的 AI 系统来说是极难做到的。
举个例子来说明。数学最古老的定理之一是欧几里得在公元前 300 年证明的质数有无穷多个。最初，欧拉发现将所有已知质数相乘后再加一总能得到一个新的质数。虽然接下来的证明过程很简单，但这个开放性想法第一次浮现时的确是一门艺术。
“你无法让计算机想出那个主意。” Buzzard 表示，至少现在还不行。
巧的玩不转，Lean采取什么方法跟人类大脑竞争呢？
Lean和所有AI算法一样，需要“喂数据”进行训练。
目前的Lean，不但无法设计出完整的IMO题目证明过程，它甚至无法理解其中一些问题所涉及的概念。
所以，Lean的首要任务是学习更多的数学知识。
训练数据来自Mathlib的库。Mathlib是一个数学基础数据库，它几乎包含了大学二年级以下所有数学知识。
但Mathlib在中学数学上仍有一些差距，团队正在对Mathlib数据库进行补全。
掌握知识只是第一步，如何灵活运用才是关键。
团队采取的方法与象棋、围棋AI等相同——遵循决策树，直到算法找到最优解。
许多IMO题目的关键是寻找某种证明的模式。深入数学证明的底层，是一系列非常具体的、有逻辑的步骤。
研究人员尝试通过IMO题目证明的全部细节来训练Lean。
但在这种方法也有局限，每个特定的题目证明对于算法来说太“专”，下一个不同类型题目仍然不会解。
为了解决这个问题，团队需要数学家写出之前IMO题目的详细形式化证明。然后，团队提炼证明中的采用的不同策略。
接下来，Lean的任务，就是在这些策略中寻找一个 “胜利 “的组合。
这项任务实际上比描述起来困难的多，团队这样比喻它：
在围棋中，目标是找到最好的一步棋。而在数学中，目标是找到最好的一盘棋，然后在这盘棋中找到最好的一步棋。
AI 能成为 IMO 冠军吗
团队说，也许到了明年，获得金牌仍然是很困难的，但至少，Lean有机会参赛了。
对此，有网友感叹AI这些年神速的进展：先是国际象棋、又是围棋……现在，AI又要来攻占国际奥赛金牌了。
网友评论截图
但也有网友持悲观态度，认为AI现阶段只能在某些方面趋近人类的水平。
目前AI的算法，都是建立在人类认知基础上的……所以像（证明数学定理）这样特殊的任务，我持消极态度，毕竟世界上只有少部分人能提供帮助。
“什么是数学思想？”
这个问题出乎意料的难以解释透彻。数学家在尝试解决新问题时，大脑的活动是难以描述的，更不要说落实在算法上。
尽管已经有AI团队朝数学思想的深层迈出了一步，但是从他们采取的策略来看，仍然是学习过往思路，选择成功率最高的“排列组合”。
这样的AI算法，要在创造力和突破性上超越人类，“火候”还差得远。
而隔壁的GPT，也在数学证明方向上取得了初步成果。
最近，OpenAI推出了用于数学问题的GPT-f，利用基于Transformer语言模型的生成能力进行自动定理证明。
由GPT-f发现的23个简短证明已被Metamath主库接收，这也是首次AI的数学证明获得业内认可。
GPT真的是要砸所有人的饭碗，连数学家都不放过。
你看好AI吗？
来源：综合自量子位、科研圈|图片：除说明外来源资料库