9月27日，第61届国际奥林匹克数学竞赛（IMO）最终比赛成绩公布，中国队以215分获得总成绩第一名。但本届比赛也非常特殊，可能会载入史册：由于新冠大流行，大赛首次远程举办，并且是最后一次没有人工智能（AI）参加的比赛。实际上，研究者们已经把IMO看作是研发智能机器的理想试验场，AI若能在这里脱颖而出，就变相证明了AI能与人类认知能力的一个重要方面相匹敌。
自1959年以来，IMO就开始每年汇集全世界最优秀的大学预科数学学生。在赛程的前两天，参与者有四个半小时的时间来解答三个难度递增的问题，其中每个问题最多可得7分。像奥运会一样，得分最高的选手也能获得奖牌。比赛的最大赢家会成为数学界的传奇人物，其中有些人后来还成为了顶尖的数学家。IMO的题目不涉及任何高等数学知识，就连微积分也被认为是超纲内容，仅从这个意义上来说，IMO并不算很难。
但是，即使难度不大，这些题目会极为复杂，比如下面这道出自1987年古巴大赛的问题。解决IMO问题通常需要灵光一现，而这正是如今AI难以跨越的第一个障碍。例如，公元前300年，欧几里得证明了有无限多个质数存在，这是数学界最古老的成果之一。我们也能意识到，总是可以通过将所有已知的质数相乘并加1来找到一个新的质数。虽然接下来的证明简单，但想出证明方法这个过程本身就可以称得上是一项艺术行为。如何训练AI？
IMO 大挑战团队正在使用一个名为Lean的软件程序，该程序由微软的研究员Leonardo de Moura于2013年首次启动。Lean作为“证明助手”，可以检查数学家的证明过程，并自动完成证明中乏味的部分。但是目前，它甚至还无法理解某些题目所涉及的概念。如果想要让Lean表现得更好，有两件事需要改变。首先，Lean需要补习数学知识。Lean使用了一个内容不断在丰富的数学库mathlib。
如今，mathlib几乎包含了数学专业的大二学生可能知道的所有内容，但是对于IMO来说还些还不够。第二个更大的挑战是教会Lean该如何利用其所拥有的知识。IMO大挑战团队希望利用遵循决策树直到找到最佳方案的方法，来训练Lean得出一项数学证明。通过这种方式，其他AI系统已经成功进行了象棋和围棋那样的复杂游戏。然而，什么是数学想法呢？这个问题出乎意料地难以回答。
对高层次来说，许多数学家在解决一个新问题时所做的事是无法理解的。为了走出这一困境，IMO大挑战团队需要数学家们为以前的IMO问题撰写详细而正式的证明。随后，团队将试图从这些证明中提炼出它们得以起作用的技巧或策略。接下来，他们将训练一个AI系统，在这些策略中进行搜索，以找到一种能够“成功”的策略组合，以解决新出现的IMO问题。
据Selsam观察，比起在最复杂的棋盘游戏中取胜，在数学竞赛中夺冠要困难得多。毕竟，AI起码能提前知道棋盘游戏的规则。他说：“也许在围棋游戏中，目标是找到最好的下棋子策略；而在数学中，目标是先找到最好的“游戏”，再找到该游戏中最好的策略。”IMO大挑战目前还是个疯狂的计划。de Moura在赛前表示，如果Lean参加了今年的比赛，那么“我们可能会得到零分”。
但是，研究人员想要在明年比赛举办之前实现一些目标。他们计划填补mathlib中的漏洞，以便Lean能理解所有的题目。他们还希望获得数十个IMO历史问题详细而正式的证明，这将成为Lean的第一本基础参考手册。等到那时，Lean便能够参加比赛，尽管它想要获得金牌可能仍然遥不可及。“目前我们做了很多事，但还没有什么实质性的进展，”Selsam说道，“明年，Lean将再接再厉。”