9月27日，第61届国际奥林匹克数学竞赛（IMO）最终比赛成绩公布，中国队以215分获得总成绩第一名。但本届比赛也非常特殊，可能会载入史册：由于新冠大流行，大赛首次远程举办，并且是最后一次没有人工智能（AI）参加的比赛。实际上，研究者们已经把IMO看作是研发智能机器的理想试验场，AI若能在这里脱颖而出，就变相证明了AI能与人类认知能力的一个重要方面相匹敌。
自1959年以来，IMO就开始每年汇集全世界最优秀的大学预科数学学生。在赛程的前两天，参与者有四个半小时的时间来解答三个难度递增的问题，其中每个问题最多可得7分。像奥运会一样，得分最高的选手也能获得奖牌。比赛的最大赢家会成为数学界的传奇人物，其中有些人后来还成为了顶尖的数学家。解决IMO问题通常需要灵光一现，而这正是如今AI难以跨越的第一个障碍。
IMO 大挑战团队正在使用一个名为Lean的软件程序，该程序由微软的研究员Leonardo de Moura于2013年首次启动。Lean作为“证明助手”，可以检查数学家的证明过程，并自动完成证明中乏味的部分。但是目前，它甚至还无法理解某些题目所涉及的概念。如果想要让Lean表现得更好，有两件事需要改变。首先，Lean需要补习数学知识。其次，教会Lean该如何利用其所拥有的知识。
IMO大挑战团队希望利用遵循决策树直到找到最佳方案的方法，来训练Lean得出一项数学证明。为了走出这一困境，IMO大挑战团队需要数学家们为以前的IMO问题撰写详细而正式的证明。随后，团队将试图从这些证明中提炼出它们得以起作用的技巧或策略。接下来，他们将训练一个AI系统，在这些策略中进行搜索，以找到一种能够“成功”的策略组合，以解决新出现的IMO问题。IMO大挑战目前还是个疯狂的计划。
de Moura在赛前表示，如果Lean参加了今年的比赛，那么“我们可能会得到零分”。但是，研究人员想要在明年比赛举办之前实现一些目标。他们计划填补mathlib中的漏洞，以便Lean能理解所有的题目。他们还希望获得数十个IMO历史问题详细而正式的证明，这将成为Lean的第一本基础参考手册。等到那时，Lean便能够参加比赛，尽管它想要获得金牌可能仍然遥不可及。