小樂數學科普：AI時代專題系列——數學之美、真理和證明——譯自Quanta Magazine量子雜志

★加星zzllrr小樂公眾號數學科普不迷路！

數學家們已經開始為數學意義的深刻轉變做準備。#AI時代專題系列

圖源：Sally Caulwell / Quanta Magazine

作者：Jordana Cepelewicz（量子雜志數學主編）2025-4-30

譯者：zzllrr小樂（數學科普公眾號）2025-5-1

自20世紀初以來，數學的核心一直是證明——一個嚴格的、合乎邏輯的論證，證明一個給定的命題是真是假。數學家的職業生涯是通過他們能證明什么樣的定理以及證明多少定理來衡量的。他們花費了大量時間提出新的見解來使證明發揮作用，然后將這些直覺轉化為一步一步的推理，像拼圖一樣將不同的推理路線組合在一起。

最好的證明都是藝術品。它們不僅嚴謹，而且優雅、富有創意且漂亮。這使它們像是一種明顯的人類活動——我們理解世界、磨礪思維、測試思維本身極限的一種方式。

但證明本質上也是理性的。因此，當研究人員在1950年代中期開始開發人工智能時，他們希望自動化定理證明是很自然的：設計能夠生成自己的證明的計算機程序。他們取得了一些成功。最早的 AI 程序之一可以輸出數理邏輯中的數十個命題的證明https://www.cs.cornell.edu/courses/cs4860/2012fa/MacKenzie-TheAutomationOfProof.pdf 。其他程序緊隨其后，想出了證明幾何、微積分和其他領域命題的方法。

盡管如此，這些自動定理證明器仍然有限。數學家真正關心的定理類型需要太多的復雜性和創造力。數學研究一如既往地繼續進行，沒有受到影響，也沒有被嚇倒。

現在，這種情況開始改變。在過去的幾年里，數學家們使用機器學習模型來發現新模式 https://www.nature.com/articles/s41586-021-04086-x ，發明新猜想，并找到舊猜想的反例。他們創建了強大的證明助手 https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ 既可以驗證給定的證明是否正確，也可以組織他們的數學知識。

到目前為止，他們還沒有構建可以從頭到尾生成證明的系統，但這種情況可能正在發生變化。2024年，Google DeepMind宣布他們開發了一種人工智能系統，該系統在IMO國際數學奧林匹克競賽（一項針對高中生的著名的以證明為主的考試）中獲得銀牌 https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ 。OpenAI更通用的“大語言模型”ChatGPT在復制證明和解決具有挑戰性的問題方面取得了重大進展，較小規模的定制系統也是如此。

“它們進步的程度令人震驚，”蒙特利爾大學的數學家安德魯·格蘭維爾（Andrew Granville）說，直到最近，他才懷疑這項技術可能很快就會對定理證明產生真正影響的說法。“它們徹底打破了我原以為存在的限制，天機已經泄露了。”

研究人員預測，他們將能夠在未來幾年內開始將更多乏味的證明部分外包給AI。對于人工智能是否能夠完全證明他們最重要的猜想，他們意見不一：一些人愿意接受這個概念，而另一些人則認為存在無法克服的技術障礙。但是，數學事業中更具創造性的方面有朝一日可能會實現自動化，這已不再完全不可能。

Andrew Granville擔心，將更嚴格的數學方面外包給AI可能會對研究人員的思考能力產生不利影響。“我意識到，自己的認知并非源自高瞻遠矚，”他說，“而是來自親力親為的實踐。”

圖源：Alex Tran / Quanta Magazine

即便如此，目前大多數數學家“都把頭牢牢地埋在沙子里，”格蘭維爾說。他們忽視了最新的發展，寧愿將時間和精力花在他們平常的工作上。

一些研究人員警告說，繼續這樣做將是一個錯誤。即使是將枯燥或死記硬背的部分證明外包給AI的能力，“隨著時間的推移，也會極大地改變我們的工作以及我們對數學的看法，”新澤西州普林斯頓高等研究所杰出數學家、菲爾茲獎獲得者阿克薩伊·文卡特什（Akshay Venkatesh，1981 -）說。

他和一小群其他數學家現在開始研究人工智能驅動的數學未來會是什么樣子，以及它將如何改變他們所珍視的東西。在這樣的未來，數學家們將扮演批評家、翻譯家、指揮家、實驗家的角色，而不是把大部分時間花在證明定理上。數學可能會更接近實驗室科學，甚至藝術和人文學科。

想象AI將如何改變數學不僅僅是一項準備工作。它迫使數學家考慮數學的真正核心是什么，以及它的用途是什么。

工具所鑄

蘇格拉底是西方最早擔憂技術如何與清晰思維相互沖突的思想家之一。在他看來，日益普及的書寫技術是一種不可靠的信息載體，會侵蝕人們與生俱來的記憶能力。

今天，我們不能不寫作就做數學。“紙張的作用是外部記憶，一種不同類型的思維系統，”Venkatesh說。它允許人們存儲知識并將其傳遞下去；甚至關于使用哪些符號來表示數學概念的決定也帶來了重要的進步。

在蘇格拉底時代以及接下來的2000年里，西方數學是幾何學。古希臘人將數學描述為關于大小的科學，即你可以繪制、測量和計數的事物。通過以幾何方式表示概念，數學家可以找到意義并發現應用。這項工作是物理的，甚至是觸覺的。

然后，在1637年，法國數學家勒內·笛卡爾（René Descartes，1596 - 1650）發表了他的論文《方法論》（Discourse on the Method https://www.gutenberg.org/ebooks/59 ）。在其附錄中，他介紹了后來被稱為笛卡爾坐標的東西：一種將幾何曲線和形狀轉換為代數方程的方法。

代數成為外包某些無法用幾何方式解決的問題的手段。但這也意味著要遠離對數學的物理理解。“你可以艱難地完成代數，但在某種程度上你是在盲目工作，”英格蘭開放大學的杰里米·格雷（Jeremy Gray）說。“機械套用之法，終不及歐氏幾何的直觀之美。”

在17世紀，勒內·笛卡爾引入了一種將幾何曲線表示為代數方程的方法。它改變了數學的完成方式。

圖源：公共領域

一些數學家認為代數方法將數學帶向了錯誤的方向。其中最主要的是艾薩克·牛頓（Isaac Newton，1643 - 1727）。他寫道，這些方法“如此乏味和糾纏，以至于令人作嘔”。對他來說，幾何直覺是真正用數學方式理解事物的核心。他聲稱 http://mitp-content-server.mit.edu:18180/books/content/sectbyfn?collid=books_pres_0&fn=9780262013178_sch_0001.pdf&id=8197 ，通過代數符號和抽象方面的工作，數學家不可能理解他們在做什么，即使他們認為自己在做什么。

起初，代數技術是達到目的的一種手段。它們只是使數學家能夠思考和解決某些問題。但很快，數學家們就開始為了他們自己而研究這些技術，從而產生了各種美麗的數學：例如，如果沒有代數，微積分是不可想象的。這反過來又導致了集合論等形式主義——現代數學的基礎——隨后開辟了全新的研究領域。（牛頓是微積分的發明者之一，最初為它開發了一個代數框架。但由于他的哲學觀點，他拒絕出版他的作品，直到他找到一種以幾何方式呈現它的方法。）

數學逐漸從其幾何根源轉為越來越抽象。“今天，數學真理以幾何學為基礎的概念似乎很古怪，”卡內基梅隆大學的杰里米·阿維加德（Jeremy Avigad）在2022年的一篇文章中寫道 https://www.ams.org/journals/bull/2022-59-01/S0273-0979-2021-01726-5/viewer/ 。數學家現在將問題外包給各種方法，包括代數和非代數；他們通常將這些比代數方程復雜得多的方法稱為數學“機械”。曾經不可接受的抽象概念現在并不比一個強大的工具更神秘，并且對于構建任何雄心勃勃的東西同樣重要。

了解每一顆釘子

為了構建證明，數學家從堅實的假設或公理基礎開始。他們一次一個地在這個基礎上放置積木 — 命題或引理，這些命題或引理最終組合在一起，幫助形成一個單一的邏輯結構。

歸根結底，重要的是這個總體結構：墻壁、樓梯和柱子賦予了證明的形狀。但是，雖然證明最有趣的方面可能是它的藍圖——論證的總體設計——但磚塊本身也很重要。引理是次要的陳述，也需要證明為真，然后以巧妙的方式組合起來，以構建完整的證明。

La Géométrie《幾何學》是笛卡爾著名的《方法論》中的一個簡短附錄，為解析幾何奠定了基礎。通過引入坐標系的概念，笛卡爾在幾何和代數之間架起了一座橋梁，后來使微積分和其他重要數學領域的發展成為可能。

圖源：公共領域

例如，一個引理可能涉及泛化一個已知的命題，或證明一個對象滿足一組特定的性質。通常，數學家有理由相信這樣的引理是正確的。但是嚴格證明它們可能需要一段時間，從幾小時到幾周不等。它們可能不需要很多創造力，但它們很耗時，并且它們最終可能會在最終的證明中占據一頁又一頁的篇幅。

幾年后，AI模型（與形式驗證系統配對以檢查準確性）可能能夠自動證明這些引理，就像數學家目前將簡單算術外包給計算機程序一樣。如果發生這種情況，論文將更容易寫。數學將發展得更快，以更快的速度開辟新的研究領域。數學教育可能會發生重大變化。

在這個愿景中，數學家將繼續成為新數學大教堂的建筑師。但他們也不必再兼任施工隊，親手打造和敲打每一塊磚、每根托梁和每顆釘子。

然而，即使是這種對人工智能的使用——實現人類已經可以做的事情，盡管速度更慢——也可能極大地改變數學，就像17世紀代數機械的引入一樣。為了了解這可能是什么樣的，倫敦帝國理工學院的希瑟·麥克白（Heather Macbeth）一直在比較傳統的證明 https://arxiv.org/abs/2405.04699 與使用證明助手 Lean編寫的相同定理的證明。

在一個Lean的證明中，所有步驟都是用計算機代碼編寫的，有些是手工編寫的，有些是使用人工智能編寫的；然后，軟件程序驗證這些步驟是否遵循有效的邏輯鏈，以及證明是否正確。Macbeth發現，在這樣的證明中，你可以將更多信息打包到稱為“策略”的自動化流程中，從而讓數學家騰出時間專注于更高層次的描述和理解。

“即使在我們認為基于證明的數學中，即成人研究數學的生計中，仍然有很多東西實際上是計算，”麥克白說。隨著證明的這些部分被外包給計算機，無論是Lean還是其他一些AI系統，數學家可以花費更多的精力來提供解釋和傳達最重要的思想；對細節的強調將減少，因為細節將成為AI的職權范圍。這將代表數學的重大文化轉變：數學家將不再需要那么多地關注嚴謹性。

“紙上的嚴謹和你頭腦中的嚴謹之間會有某種脫節，”多倫多大學的丹尼爾·利特（Daniel Litt）說。“我會從整體意義上理解一些新的東西，即使我不會理解所有的細節。”

然而，總的來說，數學家們在氣質或訓練上超乎尋常地傾向于關注嚴謹性。“我不喜歡不了解細節的感覺，所以我必須接受這種感覺，”利特說。

幾千年來，歐幾里得的《幾何原本》（Elements of Geometry）深刻影響了數學家對嚴謹性的思考。但在過去的400年里，數學變得越來越抽象。

圖源：公共領域

這種感受不僅僅是出于不適；數學家們擔心（正如蘇格拉底曾經擔憂的那樣），如果停止強調嚴謹性，可能會對他們的思維能力產生負面影響。“你或許會說，好吧，現在可以自由地關注更大的圖景了。但我認為我自己的理解并非源于宏觀視角，而是源于親自動手的實踐，”格蘭維爾說，“抽象的力量，在那些同時理解實踐的人手中才能發揮最大效力。”

分工合作

許多數學家可能會因為無法理解他們證明中的每一個細節而感到不安，但我們已經有非常成功的研究計劃的例子，在這些計劃中，沒有人可以把每一個細節都記在腦子里。例如，在粒子物理學領域，有3000多名作者在論文中宣布發現了希格斯玻色子，這是一項耗資數十億美元的科學實驗的最高成就。即使在數學領域，在20世紀的過程中，也有100多名研究人員為一項大規模證明做出了貢獻——填滿了10000多頁——將重要對象分類為有限單群。

AI將使這種數學項目成為常態而不是例外，將主題轉變為強調實驗的大型合作，并有可能提出以前無法提出的問題。

2024年秋天，為了展示未來可能是什么樣子，加州大學洛杉磯分校的陶哲軒（Terence Tao）啟動了方程理論項目 https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/ 。首先，他考慮了一個叫做原群（magma）的簡單數學對象：一組元素，以及將集合中任意兩個元素組合成第三個元素的規則。（該規則可能是加法、乘法或不太熟悉的運算。數學中最核心的對象之一，稱為群，是一種特殊類型的原群。參閱

然后，陶哲軒提出了數千個命題，描述了任何給定原群中的元素可能的行為。例如，元素可能是可交換的，這意味著你組合它們的順序無關緊要。或者將元素與自身組合在一起可能總是會得到相同的元素。陶哲軒說，每個命題“本身就是一個無聊的東西”。但他想了解所有這些命題是如何相互關聯的。如果原群滿足一個命題，它可能還必須滿足一系列其他命題，但不能滿足別的命題。

所有命題中有2200萬種可能的含義，陶哲軒想評估每一個命題是真是假。“你把這些方程式的景觀看作一件大事，你正在研究這個景觀本身，”阿爾伯塔大學的亞當·托帕斯（Adam Topaz）說，他沒有參與這個項目。“沒有計算機，我們就無法做到這一點。”

在幾個月內，50多名參與者（其中許多是業余愛好者）證明了幾乎所有2200萬條蘊含命題的真假。有些人使用了AI；其他人則手工解決。最終，該項目于2025年4月完成 https://mathstodon.xyz/@tao/114337393836459074 ，開辟了數學提問的新領域，否則看起來根本不會有趣。

這讓我們看到了AI輔助數學研究的一絲光芒。“未來，當我們探索數學的一個領域時，你可以首先讓一個AI來探索數百萬個問題，并獲得一些初步的景觀，”陶哲軒說。“只是質量很低。但這將引導更老練的人類說，‘好吧，現在，根據這種實驗，我們應該將我們的人力資源用在這里。’”

“這是一種更分散的方法，”渥太華大學的瑪雅·弗雷澤（Maia Fraser）說。或者，正如荷蘭萊頓大學的人類學家和歷史學家羅德里戈·奧內加梅（Rodrigo Ochigame）所說，“它具有這種不守紀律、實驗性、自力更生的性格。”

“我們會更像物理學家，”格蘭維爾說。“我們傾向于先說出我們的猜測，然后希望它是正確的。這是一種非常不同的方法，你很多時候都錯了，你只是偶爾希望你能達到目標。”

數學家陶哲軒提出了他的“方程理論項目”，以測試一個更具協作性、實驗性、人工智能驅動的未來會是什么樣子。

圖源：Reed Hutchinson

因此，與物理學和其他實驗室科學一樣，數學也可能涉及更多的分工。目前，數學家負責從頭到尾執行所有數學任務：提出新想法、證明引理和定理、撰寫證明并傳達它們。隨著AI的出現，這種情況很可能會改變。一些數學家可能會繼續手工做數學，而AI系統的能力存在差距。

其他數學家可能負責開發理論進行測試，或將猜想翻譯成計算機語言，以便AI和驗證系統可以投入使用，或確保AI所證明的實際上是數學家想要證明的（這是一項非常艱巨的任務），或在項目的眾多合作者之間進行協調，或向他人解釋自動證明。“在物理學或化學中，有人提出理論，有人做實驗，他們都重視對方，”烏得勒支大學和Lean研究組織的數學家約翰·科梅林（Johan Commelin）說。“它可能會開始看起來更像那樣。”

“我們將看到更多的小組項目，其中沒有一個人知道正在發生的一切，但人們可以集體完成比任何個人都多得多的成就，”陶說。“這就是現代世界其他部分的運作方式。”

數學的終結？

了解到什么算作重要的數學問題往往是一個品味問題，這可能會讓人感到驚訝。從深遠的角度來看，“什么是數學”這個問題與“數學家認為什么很重要”這個問題是一樣的。

根據Venkatesh的說法，解決某些數學問題越容易，數學家就越不重視這些問題 https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01834-5/viewer/ 。“這就像高級時裝，”DeepMind的研究員Alex Davies說。“一旦你擁有了讓人們很容易接觸到高級時裝的技術，它成為大眾市場，那么它就會變得不那么時尚。高級時尚人士去做其他事情。”

AI系統可能更適合某些問題，這使得這些問題本身就不那么有趣。目前尚不清楚哪些學科可能會先落下。例如，尋找函數的最優解的問題曾經是純數學中更核心的部分，與微積分、代數和其他領域緊密交織在一起。

但在20世紀中葉，隨著基于計算機的技術發展，優化證明往往被簡化為計算。重點轉移到這些技術的應用上，因此今天，雖然優化問題仍然很重要，但它們更多地屬于應用數學領域——這個領域不是為了它們本身而涉及對思想或概念的研究，而是旨在將它們用作實現特定、實際目的的手段。

AI可能特別適合于最優化和其他領域中往往更具體或傾向于重復使用相同類型的證明技術的問題。例如，一些數學家認為人工智能可能會改變組合學，即計數的數學研究。其他數學家認為，最容易自動化的學科是那些涉及更多符號表示的學科，例如代數。

盡管如此，如果AI足夠好，可以解決其中一些領域的問題，那么可能沒有什么可以阻止它最終擅長所有領域的問題。在那個未來，數學家可以把注意力集中在其他事情上。“我相信AI將能夠證明很多事情，但數學家只會改變他們工作的抽象層次，”Topaz說。

例如，在使用AI的過程中，Litt已經意識到，比他所意識到的要多得多的數學知識是關于了解大量事實并以有趣的方式將它們組合在一起，而不是靈光乍現。“我某種程度認為，很多困難的事情更多的是關于你的工作記憶和知識，而不是創造力，”他說。

“這動搖了我的信心，因為我明白我們做什么，或者什么是優秀的數學家。現在我認為我所做的大部分工作是將一些以標準方式已知的事實放在一起。然后每隔一段時間，我所做的實際上就會有創意部分。我做一個類比或發展一個新的定義。”

這意味著“我所做的很多事情都是機器觸手可及的，”他補充說。

也許數學家會把大部分時間花在試圖理解AI系統生成的證明上——這項任務需要大量的時間、精力和聰明才智。哈佛大學數學家馬克·基辛（Mark Kisin）預計，該領域可能會在未來10到100年內轉變為更接近人文學科。“如果你看大學的一個典型的英語系，它通常不是由寫文學作品的人組成的，”他說。“它的工作人員都是批評文學的人。”

同樣，他說，數學家可能會扮演批評家的角色，他們仔細分析AI證明，然后在研討會上教授它們。羅南·埃爾丹（Ronen Eldan）是一位數學家，最近離開了魏茨曼科學研究所去了OpenAI，他回憶起另一位數學家在一次談話中的預測，“今天的數學家將像鋼琴家一樣，”他說。“他們不演奏自己的作品，但人們仍然來聽。”

即便如此，數學家也有很多工作要做，從提出新的定義和抽象到決定哪些新的研究方向最值得追求。“我很難想象指導數學課程的基本創造性工作不是由人類完成的，”約翰霍普金斯大學的艾米莉·里爾（Emily Riehl）說。

盡管如此，數學家設想的潛在變化是深遠的。“從某種意義上說，這將是目前實踐的數學研究的終結，”利特說。“但這并不意味著這將是數學家的終結。”

“我認為這會對我的自尊心造成打擊，但我不認為我會為此感到非常沮喪，”他補充道。“如果有一個大語言模型可以證明黎曼假設 https://www.youtube.com/watch?v=zlm1aajH6gY 并向我解釋證明，我仍然會非常高興地學習它。大多數情況下，我想在數學中做的是理解什么是真的以及為什么它是真的。”

“在過去的50年里，我們有點處于靜止的環境中。我們可以繼續做我們正在做的事情，”Venkatesh說。“但我們不能再這樣做了。”

參考資料

https://www.quantamagazine.org/mathematical-beauty-truth-and-proof-in-the-age-of-ai-20250430/

https://www.quantamagazine.org/series/science-in-the-age-of-ai/

https://www.cs.cornell.edu/courses/cs4860/2012fa/MacKenzie-TheAutomationOfProof.pdf

https://www.nature.com/articles/s41586-021-04086-x

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://www.gutenberg.org/ebooks/59

http://mitp-content-server.mit.edu:18180/books/content/sectbyfn?collid=books_pres_0&fn=9780262013178_sch_0001.pdf&id=8197

https://www.ams.org/journals/bull/2022-59-01/S0273-0979-2021-01726-5/viewer/

https://arxiv.org/abs/2405.04699

https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/

https://mathstodon.xyz/@tao/114337393836459074

https://www.ams.org/journals/bull/2024-61-02/S0273-0979-2024-01834-5/viewer/

https://www.youtube.com/watch?v=zlm1aajH6gY

科普薦書

【更多讀者好評數學書單推薦、數學科普作家自薦、出版社書單推薦通道已陸續打開，敬請期待】

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

加星★

數學科普不迷路！