第61屆國際數學奧林匹克(IMO)已經結束。由于以下兩個原因，這次IMO將在比賽歷史上留下印記：因為新冠肺炎，這是第一次遠程組織的比賽，也可能是最后一次沒有AI選手的比賽。
自1959年以來，每一屆國際數學大會都匯聚了世界上最有才華的數學預科大學生。比賽分為兩天，參與者每天有四個半小時的時間回答三個問題。每道題最多可得7分，得分最高的選手將被邀請上臺領獎(通常由當代著名數學家頒發)。之前的IMO選手包括數學方面的傳奇和領軍人物。
今年團體總分冠軍是中國隊，唯一的滿分選手是來自巴蜀中學的李金珉。
現在，研究人員將IMO視為人工智能的理想測試場所。如果AI系統能夠解決問題，那么它其實就擁有了以前只有人類才有的認知能力。
事實上，當人工智能(AI)的概念第一次出現時，當時的科學家猜測AI最適合解決數學問題，因為數學問題可以用嚴格的形式語言來表達，比如寫劇本、寫詩等文學活動，甚至人類的日常交流。我們使用的語言太模糊，缺乏清晰的定義。
然而實際發展卻超出了大家的預期。AI雖然無法創作出堪比人類的作品，但在一定空間內迷惑人類批評家——，讓他們相信文字都是來自其他人類，就足夠了。另一方面，到目前為止，沒有一個AI系統能夠獨立解決一個數學問題。
的確，計算機更擅長計算。但只有當它們作為工具使用時，才能通過人類設定的算法給出有意義的答案。的確，所有的數學知識都可以用形式語言嚴格定義，數學推理本身遵循形式邏輯。然而，邏輯并不能幫助我們找到數學證明的關鍵。其實回憶初中的平面幾何——，想要證明結論，需要找到正確的輔助線，但不是在推導輔助線的連接方法。其實是經驗、試錯、內在數學形象的結果。邏輯推理本身只是在核對證明思路，寫出清晰證明的過程中起作用。
例如，數學上最古老的最大結論之一是西元前300年的歐幾里得證明，存在無限多個質數。首先要認識到，如果質數是有限的，則總是可以通過將所有已知的質數相乘并加1來找到一個新的質數。證明本身并不難，但現有的AI幾乎永遠也無法獨立想出這一方法。
或者，你可以嘗試解決今天的心理體操。想好AI會怎么想，再想出答案。
微軟研究院的丹尼爾塞爾薩姆說：“對我來說，國際海事組織代表著最困難的挑戰。”塞爾薩姆是IMO大挑戰的創始人。項目目標是訓練AI系統在IMO比賽中獲得金牌。
IMO大挑戰團隊使用了微軟研究員萊昂納多德莫拉(Leonardo de Moura)在2013年開發的名為Lean ——的程序。原本是一個“證明助手”，可以幫助考查數學家的論文，自動填寫證明中枯燥重復的細節。
該團隊將向Lean添加一個巨大的數學庫mathlib。如今，不斷增長的數學圖書館幾乎涵蓋了從小學到數學專業二年級可能知道的一切，但遠遠不夠。
當AI配備了必要的工具。挑戰團隊希望通過訓練AI來學習已有的證明，開發可用的決策樹，并學習使用庫中已有的定理來證明未知的結論。
雖然AI在各種棋類游戲中已經遠遠超過了人類頂尖選手，但從本質上來說，數學研究或者中學生數學競賽也是一項比象棋更復雜更微妙的活動(象棋目標明確單一，規則簡單，一般遵循統計對策……這些對AI都很友好)。
塞爾薩姆說：“在圍棋中，AI的目標是找到最好的一步，而在數學中，AI的目標是找到最好的游戲，然后在游戲中找到最正確的打法。如果讓我們的AI參加今年，那也只會以0分結束.現在繼續發展，明年就有機會了。”
https://www . quantamagazine . org/at-the-international-mathematic-Olympic ad-manual-intelligence-prepared-to-go-for-the-gold-20200921/