人工智能
明年的IMO或将有AI选手参赛
第61届国际数学奥林匹克竞赛(IMO)已然落幕。因以下两个原因，本届IMO或将在赛会历史上留下一笔：由于COVID-19，这是首届远程组织的赛会，也可能是最后一届没有AI参赛者的赛会。
自1959年以来，每届IMO都汇集了世界上数学方向上最有天赋的预备大学生。比赛分两天，参与者每天有四个半小时的时间来回答3个问题。每个问题最多可得7分，得分最高的选手将被邀请到台上领奖(一般由当代著名的数学家亲手颁发)。IMO历届选手包括如今数学界的传奇和领军人物。
今年团体总分冠军是中国队，唯一的满分选手是来自巴蜀中学的李金珉。
现在，研究人员视IMO为AI的理想试验场。如果AI系统能够解答出题目，那它实际上就拥有了以前只有人类才有的认知能力。
实际上，当人工智能(AI)的概念最早出现的时候，当时的科学家猜测，AI最适合用来解决数学问题，因为数学问题是可以用严格的形式语言来表述的，像是撰写戏剧、诗歌等文艺活动，乃至人类的日常交流，我们用到的语言太过含混模糊，缺少明晰的定义。
但是，实际发展却超出了所有人的预料。虽然现在的AI还无法创作出可以堪比人类的作品，但足以在一定篇幅内迷惑住人类批评家——让他们相信文字都是出自其他人类。另一方面，至今还没有哪个AI系统能够独立解决某个数学问题。
确实，计算机长于计算。但它们只有在作为工具的时候，经由人类设定好算法，才能给出有意义的答案。确实，全部的数学知识都是可以使用形式语言来严格定义，同时数学推理本身也是遵循形式逻辑的。但，逻辑并无助于我们找到数学证明的关键。实际上，回忆一下初中的平面几何——要想证明结论，需要我们找到正确的辅助线，但我们并不是推理出辅助线的连法。实际上，那是经验+试错+内心的数学图像+灵光咋现，共同酝酿而成的结果。逻辑推理本身，只在检验证明思路和写出清晰证明过程中发挥作用。
例如，数学上最古老的最大结论之一是公元前300年的欧几里得证明，存在无限多个质数。首先要认识到，如果质数是有限的，则总是可以通过将所有已知的质数相乘并加1来找到一个新的质数。证明本身并不难，但现有的AI几乎永远也无法独立想出这一方法。
或者，大家可以尝试解答今天的脑力小体操。想一想要是AI会如何思考，才能想出答案。
微软研究院的Daniel Selsam说：“对我来说，IMO代表了最艰巨的挑战。”Selsam是IMO大型挑战赛(IMO Grand Challenge)的创始人，项目目标是训练AI系统在IMO竞赛中拿到金牌。
IMO Grand Challenge团队使用一个名为Lean的程序——于2013年由微软研究员Leonardo de Moura开发。原本是“证明助手”，可以帮助审查数学家的论文并自动补完证明里的乏味重复的细节。
团队要为Lean添加一个庞大的数学库mathlib。如今，还在不断增长的数学库几乎涵盖了从小学到数学专业大学二年级时可能知道的所有内容，但是还远远不足。
当为AI配备了必要的工具后。挑战团队希望通过训练AI学习已有的证明，发展出可用的决策树，学会利用库中现有定理证明未知的结论。
虽然AI已经在各种棋类博弈中远远超越了最顶尖的人类选手，但是就本质层次上而言，数学研究，或者中学生的数学竞赛也是比下棋更为复杂微妙的活动(棋类有明确单一的目标，简单的规则，大致上遵循统计的对策……这些对AI是很友好的内容)。
Selsam说：“在围棋里，AI的目标是找到最好的一步，而对数学，AI的目标是找到最佳游戏，然后在游戏里的找到最正确的玩法。如果今年让我们的AI参赛的话，它只会以0分收场……现在继续发展，明年我们才有那么点机会。”
https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/