奥数竞赛首次迎来AI选手，目标瞄准金牌，中国世界第一或受挑战

刚刚获得2020年国际数学奥林匹克竞赛（IMO）世界第一的中国队怎么也没想到，明年或将迎来一个强劲的对手，这个对手“非人类”，而是微软的机器人Lean。

当然，这个参赛的机器人不像围棋比赛一样对弈，而是作为参赛选手参与IMO，与中国队、俄罗斯队、美国队等共同争夺金牌。

还记得4年多前的那场围棋界的人机大战吗？

2016年3月，阿尔法围棋（AlphaGo）一系列比赛中，以4比1击败了世界上最顶尖的韩国棋手李世石，是第一个击败人类职业围棋选手、第一个战胜围棋世界冠军的人工智能机器人。观看由这个事件拍成的纪录片，人们很难忘记李世石被击败时的悲伤表情。从那时起，人工智能替代人类的争论就不绝于耳。

更远的事件是20多年前，1997年，IBM的深蓝国际象棋电脑在国际比赛中击败了当时的世界冠军加里•卡斯帕罗夫，人工智能的公众形象由此大幅提升，开始受到普遍关注。

人们不禁要问，明年的国际数学奥赛，数学界的天才少年是否会被机器人打败呢？

据“量子位”介绍，微软的研究人员从2013年就开始研发Lean，希望让AI能拥有自主判断、根据假设进行演绎的能力。其创始人之一微软研究员Selsam表示，其目的是训练一个人工智能系统，以便在世界顶级数学竞赛中赢得金牌。

如果AI能像人一样证明这些复杂的数学定理，某种程度上也能说明，让它“像人一样思考”就会成为可能。

中国队自1985年组队参加国际奥赛以来，共获得过21次世界第一，获得36次满分，无疑是国际数学奥赛的霸主。前几年，美国3次夺得冠军榜首，虽然中国队虽未跌出前三，但一直与冠军宝座失之交臂。直到去年和美国队并列第一，今年更是位居全球第一。

但Lean机器人显然是有备而来，经过7年的不断研发，目前已经更新到第四代，其“深度学习”的能力已非同一般。

当然，数学竞赛毕竟与围棋不同，这个项目的研发团队低调地表示，明年Lean机器人获得金牌仍然是很困难的，但至少Lean将参赛，这就是历史性的一步。

很多网友感叹说，AI这些年发展神速，从国际象棋到围棋，如今是最难的奥赛数学题。也许，终究有一天，人类大脑的工作原理会被解开，到那时，人工智能会不会取代人？