【文/觀察者網(wǎng)專欄作者 潘禺】

今年，一場數(shù)學(xué)競賽初賽結(jié)果的出圈傳播，導(dǎo)致了媒體的聚焦和全社會的討論。而在該事件不久之后，其實還有另外一場數(shù)學(xué)競賽的結(jié)果，具有深遠(yuǎn)的影響和重要的意義，在媒體上得到的關(guān)注卻小得多。那就是2024年的國際數(shù)學(xué)奧林匹克競賽 （IMO），主角中同樣有科技互聯(lián)網(wǎng)巨頭的身影，Google DeepMind的人工智能AlphaProof和AlphaGeometry 2，答對了6道題中的4道，首次達到了IMO銀牌獲獎?wù)叩乃健?

AlphaProof解決了2道代數(shù)問題和1道數(shù)論問題，包括本屆IMO中最難的問題，只有5名參賽者解決了這個問題。AlphaGeometry 2證明了幾何問題，而2個組合問題AI沒能解決。每道題最高可得7分，總共最高42分。人工智能的最終得分為28分，在解決的每個問題上都獲得了滿分，相當(dāng)于銀牌類別的最高水平，因為今年的金牌從29分開始。

這一結(jié)果表明，AI處理復(fù)雜數(shù)學(xué)推理能力有了顯著飛躍。而數(shù)學(xué)推理是人類認(rèn)知能力的一個重要方面，推動了科學(xué)發(fā)現(xiàn)和技術(shù)進步。

對中國來說，這一結(jié)果也意味著重大的機遇和挑戰(zhàn)。

中國的人工智能企業(yè)在一些領(lǐng)域處于領(lǐng)先地位，比如圖像識別。這是因為，人臉識別、物體檢測、醫(yī)療影像分析等許多技術(shù)成果，已經(jīng)應(yīng)用在支付、安防、智慧零售、交通監(jiān)控和智能醫(yī)療等，相比于AI的其它應(yīng)用領(lǐng)域，是率先落地的。又得益于中國巨大的人口規(guī)模和豐富的應(yīng)用場景，加上基建項目的政策與資金支持，中國企業(yè)能積累大量的圖像數(shù)據(jù)，進而推動了模型的訓(xùn)練和算法的優(yōu)化，在各類國際比賽中處于領(lǐng)先。

下一個在中國能廣泛應(yīng)用于實際場景的AI領(lǐng)域是哪里呢？有潛力的肯定包括智能網(wǎng)聯(lián)車和文體教等，這些也是國內(nèi)企業(yè)投入的重點。中國社會歷來高度重視教育，家庭在教育上的投入巨大，學(xué)區(qū)房、課外輔導(dǎo)、留學(xué)費用等占到了許多家庭支出的大頭。AI對教育的改變，將深刻沖擊中國社會，數(shù)學(xué)這一被中國人視為重中之重的基礎(chǔ)學(xué)科，又是我們觀察這種影響的一個窗口。

從計算到證明

雖然數(shù)學(xué)一直被稱為人類心智的榮耀，但人類使用機器作為數(shù)學(xué)的輔助，有著幾千年的歷史。

早在公元前2400年，類似算盤這樣的工具就已經(jīng)被發(fā)明。17世紀(jì)的科學(xué)家和發(fā)明家布萊茲·帕斯卡（Blaise Pascal）發(fā)明了早期的機械計算器，這種機器可以進行簡單的加減運算。20世紀(jì)60年代，第一臺電子計算器問世。早在20世紀(jì)70年代到80年代，世界上的部分高中和大學(xué)考試就開始允許學(xué)生使用計算器，90年代起，許多國家的教育體系開始正式將計算器作為教學(xué)工具，并編寫了相應(yīng)的課程，鼓勵學(xué)生使用計算器進行復(fù)雜運算。

美國的SAT數(shù)學(xué)考試在1994年首次允許學(xué)生使用計算器。目前，世界許多國家的標(biāo)準(zhǔn)化數(shù)學(xué)考試，如AP數(shù)學(xué)考試、SAT、ACT以及國際數(shù)學(xué)競賽，允許考生使用特定類型的計算器。用計算器可以幫助學(xué)生專注于數(shù)學(xué)概念的理解，而非繁瑣的計算，這已經(jīng)沒有太大爭議。中國的基礎(chǔ)數(shù)學(xué)教育以嚴(yán)格和系統(tǒng)著稱，中國學(xué)生在PISA這類國際數(shù)學(xué)評估中的表現(xiàn)十分優(yōu)異，盡管我們注重學(xué)生的計算能力，但也并不在高考中排斥計算器的使用。

機器幫助人類解決數(shù)學(xué)計算，無論在日常生活、教學(xué)還是科研領(lǐng)域，都已經(jīng)被普遍接受。強大的數(shù)學(xué)計算工具如MATLAB、Mathematica、Maple已經(jīng)是許多人工作的必備，適合簡單數(shù)學(xué)運算和統(tǒng)計分析的Excel更是普及。而在數(shù)學(xué)證明上，目前機器也在發(fā)揮越來越大的作用，這正是巨大變革可能產(chǎn)生的開始。

這次在IMO 2024，數(shù)學(xué)家陶哲軒做了一場演講，回顧了從早期計算工具到現(xiàn)代的機器學(xué)習(xí)，數(shù)學(xué)研究的范式轉(zhuǎn)變。他談到了許多例子，心智觀察所在這里結(jié)合自己的理解做一些總結(jié)和評論。

第一個例子是表格。數(shù)學(xué)領(lǐng)域的許多重要成果都是通過數(shù)論中的表格首次發(fā)現(xiàn)的，許多猜想也是通過大量的表格發(fā)現(xiàn)的。表格可以理解為數(shù)據(jù)庫，計算機的一個基本用途就是建立這些有用的數(shù)據(jù)庫。比如，很多數(shù)學(xué)家，包括陶哲軒自己，使用一個叫做“整數(shù)序列在線百科全書”（Online Encyclopedia of Integar Sequences，OEIS）的數(shù)據(jù)庫。

第二個例子是科學(xué)計算。比如用計算機來建模各種事物，求解大量線性方程或偏微分方程，這幾乎是現(xiàn)代科學(xué)研究和工程應(yīng)用的基石，從天氣預(yù)報到風(fēng)洞實驗，從新材料和藥物的研發(fā)到期權(quán)定價、核反應(yīng)堆設(shè)計，其應(yīng)用無處不在。

另一種科學(xué)計算是SAT求解器，可以解決一些邏輯難題（布爾可滿足性問題），其原理是通過檢查大量的布爾變量，尋找是否存在一組變量的賦值，使得整個布爾公式為真。通俗地說，比如給你1000個陳述，有的是真的，有的是假的，再給你一些限制條件、變量和法則，讓你證明某些句子的組合邏輯上是真的。通過把數(shù)學(xué)問題，比如畢達哥拉斯三元組問題，轉(zhuǎn)換為布爾邏輯問題，利用SAT求解器強大的組合求解能力，能夠有效尋找整數(shù)解。

第三個例子是形式化證明輔助。四色定理（任一地圖只用四種顏色就能讓相鄰的國家染上不同的顏色）和開普勒猜想（在三維空間中最有效地堆疊球體，以最大限度填充空間）的證明，都是計算機輔助證明的著名例子。

為了更加簡潔地形式化復(fù)雜的證明過程，數(shù)學(xué)家開始使用Lean平臺，Lean將數(shù)學(xué)命題用形式化語言表達并通過計算機驗證，使得每一個推理步驟都可以自動檢查。這為數(shù)學(xué)研究提供了極大的便利，也降低了證明復(fù)雜定理的出錯率。目前本科數(shù)學(xué)課程中的基礎(chǔ)內(nèi)容，比如微積分、群論或拓?fù)鋵W(xué)的基本概念等，都已經(jīng)被形式化，更多數(shù)學(xué)領(lǐng)域的內(nèi)容也在被加入到這個庫中。

數(shù)學(xué)家Peter Scholze就利用Lean試圖形式化驗證自己的高深數(shù)學(xué)理論，這些理論需要高層次數(shù)學(xué)背景和對非常抽象的概念的理解，涉及到對現(xiàn)代代數(shù)幾何、范疇論、同調(diào)代數(shù)和拓?fù)鋵W(xué)的深入掌握。Scholze對自己的證明存有疑慮，也沒有人有本事詳細(xì)查看其中的細(xì)節(jié)。Lean的形式化證明如果能夠成功，意味著形式化數(shù)學(xué)能處理現(xiàn)代數(shù)學(xué)的前沿問題。用Lean證明費馬大定理的項目，目前也已經(jīng)獲得資助并啟動。

陶哲軒自己則致力于以眾包方式來用Lean探索數(shù)學(xué)。其方法是為大型的復(fù)雜證明編寫一個藍圖，將證明分解成數(shù)百個小步驟，每個步驟都可以單獨形式化，然后組合起來，最后將長達數(shù)萬行的形式化證明轉(zhuǎn)換回人類可讀的版本，最后這步也是計算機自動生成的。

這樣的好處是，證明過程更加開放，讓數(shù)學(xué)家們可以更好地分工合作，每個人處理任務(wù)圖中自己負(fù)責(zé)的部分，通常是自己擅長解決的，而不需要理解整個證明。由于Lean可以自動檢查，就能保證每個人的工作達到質(zhì)量標(biāo)準(zhǔn)。另外，遇到修改，編譯器會自動指出關(guān)聯(lián)的地方，不需要像傳統(tǒng)的方式重寫整個證明，效率大大提高。

最后一個例子就是當(dāng)下炙手可熱的機器學(xué)習(xí)。