數學的本質是什麼？數學家渴求的客觀性真理是否能實現？人工智慧等的發展和在數學中的應用會對數學產生什麼樣的影響？本文中數論學家 Andrew Granville 探討了數學的真正本質以及為什麼客觀性永遠無法完全實現。

Andrew Granville 在蒙特利爾大學校園內。

2012 年，數學家望月新一聲稱已解決了 abc 猜想，這是數論中一個關於加法和乘法關係的難題。但有一個問題：他的證明超過了 500 頁，完全晦澀難懂。論文依賴於一堆新的定義、符號和理論，幾乎所有的數學家都覺得無法理解。多年後，當兩位數學家將證明的大部分內容翻譯成更為熟悉的數學語言時，他們指出了被其中一位數學家稱之為「嚴重且無法修復的漏洞」的邏輯問題，而望月新一則以他們未能理解他的工作而拒絕了他們的觀點。

這一事件引發了一個基本問題：什麼是數學證明？我們傾向於將其視為某種永恆真理的揭示，但也許更好地理解它是一種社會構建。

蒙特利爾大學數學家 Andrew Granville 最近一直在思考這個問題。在一位哲學家聯繫他討論關於他的一些寫作後，他說：「我開始思考我們如何得出自己的真理。一旦你開始探討這個問題，你會發現這是一個廣泛的主題。」

Granville 從小就喜歡算術，但他從未考慮過從事數學研究的職業。他的父親 14 歲就輟學了，母親在 15 或 16 歲時輟學，他的父母出生在倫敦當時的工人階級區域，大學教育對他們來說似乎是遙不可及的。所以當時全家對數學一點都不了解。

在劍橋大學數學專業畢業後，他將 Martin Amis 的小說《The Rachel Papers》改編成電影劇本。在努力推進項目並尋求資金支持的過程中，他想避免找一個坐辦公桌的工作 。在高中和大學之間的一年間，他曾在一家保險公司工作，不想再回學校。但他的這部電影從未起步（後來小說被獨立拍成電影），但 Granville 獲得了數學碩士學位，然後搬到加拿大完成博士學位。

Andrew Granville 直言讀博是自己的一次冒險，而且沒有抱很大的期望，甚至他都不知道什麼是博士學位！

但在此後的幾十年中，他發表了 175 多篇論文，大部分是關於數論的。他還因為向廣大讀者撰寫數學文章而廣受歡迎，在 2019 年，他與做編輯的姐姐 Jennifer 合作，共同創作了一本關於素數和相關概念的圖書。上個月，他的論文《How We Arrive at Our Truths》被髮表在《數學與哲學年刊》上。與其他數學家、電腦科學家和哲學家一起，他計劃在明年的《美國數學學會通報》上發表一系列關於機器如何改變數學的文章。

下面量子雜誌對與 Granville 的對話進行了一番整理。

為什麼最近發表了一篇關於數學證明性質的論文？出發點是什麼？

Granville 回答道，數學家進行研究的方式通常很難討好大眾媒體。人們往往把數學看作是一種純粹的追求，其實數學家只是通過純思維來得出偉大的真理。但數學是關於猜測的 —— 通常是錯誤的猜測。這是一個實驗性的過程。

例如，當黎曼猜想首次出現在 1859 年的一篇論文中時，它就像是魔法一樣：突然出現了這麼個驚人的猜想！之後長達 70 年的時間裡，人們一直在談論偉大的思想家如何僅靠純思維所能做到的事情。然後數學家 Carl Siegel 在哥廷根檔案館裡發現了黎曼的手稿。黎曼實際上進行了對黎曼函數零點的大量計算。

因此，人們在書寫關於數學的方式上存在這種緊張關係，特別是一些哲學家和歷史學家。他們似乎認為數學家是一種純粹的、神奇的生物，是科學的獨角獸。但通常情況下其實並不是，純粹的思維其實很少發生。

Granville 翻閱著一本名為《Prime Suspects》的圖書小說，這本小說是他與他的姐姐合作撰寫的，故事以數學為主題。

如何描述數學家所做的工作？

數學的文化完全是關於證明的。數學家坐在那裡思考，所做的 95% 都是證明。他們獲得的很多理解都來自於努力證明和解釋在努力證明時出現的問題。

大眾通常認為證明是一種數學論證。通過一系列邏輯步驟，它證明了一個給定的陳述是真實的。對於論文中提到「這不應該被誤解為純粹的客觀真理」，這句話要怎麼理解？

證明的主要目的是說服讀者陳述的真實性，這意味著驗證至關重要。數學擁有的最好的驗證系統是許多人從不同的角度看待證明，而且它在他們知道和相信的背景下很合理。在某種意義上，我們並不是在說我們知道它是真的。我們在說我們希望它是正確的，因為很多人從不同的角度嘗試過。證明是通過這些數學家團體的標準來接受的。

然後還有客觀性的概念，確保所聲稱的是正確的，感覺自己擁有終極真理。但我們如何知道我們是客觀的呢？很難將自己從提出陳述的背景中抽離出來，在社會建立的正規化之外擁有一個視角。這對於科學觀念和其他任何事情都是一樣。

人們還可以問數學中什麼是客觀有趣或重要的，但這也顯然是主觀的。為什麼我們認為莎士比亞是一位優秀的作家？莎士比亞在他那個時代並不像今天這樣受歡迎。顯然，關於什麼是有趣的、什麼是重要的存在著社會習慣，這取決於當前的正規化。

Granville 繼承了其同事的這本 19 世紀的數學著作，《The 1811 Cribrum Arithméticum》由 Ladislaud Chernac 著。

在數學中，這是什麼樣的呢？

正規化變革的最著名例子之一就是微積分。當微積分被髮明時，它涉及將一個趨近於零的量除以另一個趨近於零的量，導致零除以零，這沒有任何意義。最初，牛頓和萊布尼茲提出了無窮小的概念。這讓他們的方程式有效，但按照今天的標準來看，這並不合理或嚴格。

現在，我們有了在 19 世紀末引入的 ε-δ 形式。這種現代表達方式非常明顯地適用於正確理解這些概念，以至於當你看舊的表達方式時，你會想，他們當時是怎麼想的？但在當時，那被認為是唯一的方法。為了公平對待萊布尼茲和牛頓，他們可能會喜歡現代的方法。但受限於那個時代的正規化，他們沒有想到這樣做。所以要達到這一點花費了很長時間。

問題在於，數學家不知道自己何時在表現出這種行為。數學家被困在了自己所在的社會中。沒有外部的視角來說出數學家正在做出什麼假設。數學中的一個危險是，你可能認為某些東西不重要，因為它在你選擇使用的語言中不容易表達或討論。但這並不意味著你是對的。

笛卡爾曾經說過，「我認為我對三角形了解一切，但誰能說我真的了解？我是說，未來可能會有人提出一種截然不同的視角，從而更好地理解三角形。」他的這句話是正確的，因為在數學中，你很會經常看到這一點。

論文中有提及可以將證明視為一種社會契約，一種作者與數學界之間的共識。已經出現一個極端的例子，這種方法不起作用，就是望月新一關於 abc 猜想的證明。

這是個極端的例子，因為望月新一併不想按照通常的方式來進行這場比賽，他選擇了模糊不清。當人們取得重大突破，提出全新而複雜的想法時，他們有責任以儘可能易於理解的方式來解釋自己的想法，從而包容其他人。而他更像是說，如果你不想按照我寫的方式來讀它，那不是我的問題。他有權按照自己想要的方式來進行這場比賽。但這與數學社區無關，與數學家取得進展的方式無關。

「我們繼續努力證明我們能證明的東西，」 Granville 說。

如果證明存在於社會背景中，那麼它們如何隨著時間的推移而改變？

一切都始於亞里士多德，他說需要有某種演繹系統。你只能通過基於你已知並確定的東西來證明新事物，回溯到某些 「原始命題」或公理。

所以問題是：那些你知道是真實的基本事物是什麼？很長一段時間以來，人們只是說，線是線，圓是圓；有一些簡單明瞭的事物，那些應該是我們出發點的假設。

這種觀點已經存在了很長時間。在很大程度上在如今仍然存在。但是發展起來的歐幾里得公理系統：「一條線是一條線」，也有它的問題。基於集合概念，伯特蘭・羅素發現了一些悖論。此外，人們可以在數學語言中玩文字遊戲，創建問題陳述，如「這個陳述是假的」（如果它是真的，那麼它是假的；如果它是假的，那麼它是真的），這表明了公理系統存在問題。

所以，羅素和阿爾弗雷德・懷特海德試圖創建一種可以避免所有這些問題的新數學系統。但這個系統非常複雜，很難相信這些是正確的出發點。沒有人對此感到滿意。像證明 2+2=4 這樣的事情從出發點需要大量的空間。這樣的系統有何意義？

然後大衛・希爾伯特出現了，有了這個了不起的想法：也許我們根本不應該告訴任何人應該從什麼開始。相反，任何有效、簡單、連貫、一致的出發點，都值得探討。你不能從你的公理中演繹出互相矛盾的兩個事物，而且你應該能夠用所選的公理來描述大多數數學。但你不應該在先驗上說這是什麼。

20 世紀初，數學家們開始意識到可能存在多種公理系統：一個給定的公理系統不應被視為普遍或不言而喻的真理？

希爾伯特開始並不是出於抽象的原因而這樣做的。他對不同的幾何概念非常感興趣：非歐幾何學。這是非常有爭議的。當時的人們說，如果你給我一個定義線的方式，讓它繞過一個盒子的角，我為什麼要聽你的？希爾伯特說，如果他能夠使其連貫和一致，你應該聽，因為這可能是我們需要理解的另一種幾何學。這種觀點的變化 —— 你可以允許任何公理系統 —— 不僅適用於幾何學，它適用於所有數學。

但當然，有些東西比其他東西更有用。所以我們大多數人都使用相同的 10 個公理，這個系統叫做 ZFC（策梅洛 – 弗蘭克爾集合論 Zermelo-Fraenkel Set Theory，含選擇公理時常簡寫為 ZFC）。

這就引出了什麼可以從中演繹出來，什麼不能的問題。有一些陳述，比如連續性假設，不能使用 ZFC 來證明。必須有第 11 個公理，而且你能以兩種方式解決它，因為你可以選擇自己的公理系統。這相當酷。我們繼續保持多樣性。不清楚什麼是對的，什麼是錯的。根據庫爾特・哥德爾的說法，我們仍然需要基於品味來做選擇，而且我們希望我們有好的品味。數學家應該做有道理的事情，而且他們也確實這樣做了。

哥德爾對數學公理系統也是相當重要的角色

要討論數學，你需要一種語言和在這種語言中遵循的一組規則。在 20 世紀 30 年代，哥德爾證明，無論你如何選擇你的語言，總會有在那種語言中為真但不能從你的起始公理中證明的陳述。實際上比這更復雜，但仍然存在這個哲學困境：如果你不能證明它，那什麼才是一個真實的陳述？

這是一個大麻煩，我們在自身所能做的方面有限。專業數學家在很大程度上忽視了這一點。數學家專注於可行的事情。正如彼得・薩納克經常說的那樣，「我們是工作的人。」數學家繼續努力證明其所能證明的東西。

「數學中的一個危險是，你可以將某事看作不重要，因為它在你選擇使用的語言中不容易表達或討論。這並不意味著你是對的，」 Granville 說。

目前不僅僅是計算機，甚至人工智慧，都應用到數學，那麼證明的概念正在發生變化嗎？

現在已經進入了一個不同的領域，計算機可以做一些不同尋常的事情。現在人們說，哦，我們有這臺計算機，它可以做人類無法做到的事情。但它真的可以嗎？它真的可以做人類無法做到的事情嗎？早在 1950 年代，艾倫・圖靈說過，計算機被設計用來做人類可以做的事情，只是更快而已。並沒有太多改變。

數十年來，數學家一直在使用計算機來進行計算，以幫助引導他們的理解等。人工智慧可以做的新事情是驗證我們認為是真實的事情。我們已經在證明驗證方面取得了一些令人振奮的進展，比如「證明助手」Lean，它讓數學家能夠驗證許多證明，同時也幫助作者更好地理解他們自己的工作，因為他們必須將一些想法分解成更簡單的步驟，以供 Lean 進行驗證。

但這是百分之百可靠的嗎？只要 Lean 同意它是一個證明，那麼它就是一個證明嗎？在某些方面，它取決於將證明轉化為 Lean 輸入的人的能力。這聽起來很像做傳統數學的方式。不是說像 Lean 這樣的東西會產生很多錯誤，只是不確定它是否比大多數人類做的事情更安全。

計算機可以成為正確完成任務的非常有價值的工具，特別是對於驗證嚴重依賴於不容易在第一眼分析的新定義的數學。毫無疑問，擁有新的觀點、新的工具和新的技術對我們的「武庫」是有幫助的。但我回避的是以下這種概念：我們現在將擁有能夠產生正確定理的完美邏輯機器。

必須承認，數學家不能確定計算機的結果是正確的。數學的未來必須依賴於整個科學歷史上一直依賴的科學社群的意識：互相交流意見，與那些從完全不同角度看同一問題的人交談，等等。

未來隨著這些技術變得更加複雜，它們會發展到何種程度？

也許它可以幫助創建一個證明。可能若干年後，我們對像 ChatGPT 這樣的人工智慧模型說「我很確定我在某個地方看到過這個問題。你能檢查一下嗎？」，它可能會回覆一個相似但正確的陳述。

然後，一旦它變得非常擅長這一點，也許你可以再進一步說「我不知道怎麼做這個，但有沒有人做過類似的事情」。也許最終，一個人工智慧模型可以找到搜尋文獻的熟練方法，以運用已經在其他地方使用過的工具。這是一個數學家可能無法預見的方式。

但是 ChatGPT 如何在超越數學家的情況下進行證明，這個讓人比較難理解。ChatGPT 和其他機器學習程序並沒有思考，它們是基於許多示例的詞彙聯想。因此，它們似乎不太可能超越它們的訓練資料。但如果發生這種情況，數學家將怎麼辦呢？數學家所做的許多事情都是證明。如果你從數學家這裡拿走了證明，那麼數學家會成為什麼樣子呢？

無論如何，當我們考慮將計算機輔助應用到哪裡時，我們需要考慮從人類努力中學到的所有教訓：使用不同的語言、共同工作、持有不同的觀點的重要性。不同社群聚集在一起共同研究和理解一個證明時，呈現出健壯性、健康性。如果數學家要在數學中使用計算機輔助，需要以同樣的方式豐富它。

原文連結：https://www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/