AI幫助處理大量計算 數學家卻不滿「數學淪算術」

歐基里德的「幾何原本」2000多年來一直是數學論證和推理的典範，直到20世紀數學家們不願再將數學建立在直觀的幾何基礎，而開發系統使數學能夠轉化為電腦代碼。現在，數學家們正應對最新的變革力量：人工智慧(AI)。

紐約時報報導，澳籍華人數學家、洛杉磯加州大學數學系終身教授、菲爾茲獎得主陶哲軒(Terence Tao)表示，直到近幾年數學家們才開始擔心AI的潛在威脅，無論是在數學美學方面還是數學家本身。他說，知名的數學家們現在正提出這些問題，並探索潛在的「打破禁忌」。

他可能指的是「證明助手」(Proof Assistant)或互動式定理證明(interactive theorem prover)的程式，也就是數學家將證明一步步轉為代碼，再輸入該程式，讓電腦檢查推導是否正確，如微軟的「Lean」已經幫助證明了一些定理。驗證過程會累積在資料庫中，讓其他人可以參考。「證明助手」也有缺點：經常抱怨它不理解數學家輸入的定義、公理或推理步驟，因此得到「證明抱怨者」(proof whiners)的綽號。

但是數學家們早已出現分歧：用電腦來證明定理，是否還能稱作數學？1976年的四色定理(four color theorem，四種顏色可以填滿地圖而使所有相鄰區域顏色不重複)是首個主要藉助電腦證明的定理，一開始並不為許多數學家接受。他們認為「只是計算而非證明」，純粹是用電腦暴力破解人力無法驗證的龐大計算量。儘管電腦驗證接受度愈來愈高，但還是有人希望能找到簡潔優美的證明。

卡內基梅隆大學電腦科學助理教授賀勒博士(Marijn Heule)便稱這類工具為「暴力推理」，不過他很樂意使用。他和他的一位博士生今年2月在陶哲軒舉辦的研討會上發表一個長期難題的解方，文件大小高達50兆位元組(TB)；而這並非最高紀錄，他和其他夥伴2016年就秀出200 TB的數學證明。賀勒認為這種方法是「解決人類無法解決的問題」所必需的。