本文發表於《大眾科學》的前部落格網路，反映了作者的觀點，不一定反映《大眾科學》的觀點
這是最初發表在美國數學學會聯合數學會議部落格上的一篇文章的修訂版本。
本月早些時候，我參加了在西雅圖舉行的聯合數學會議（JMM）。 我喜歡參加JMM的原因之一是，我可以瞭解一些我不熟悉的數學領域的最新動態。 今年，我參加了一個名為“數字時代的數學資訊”的分會場中的兩個講座，這引發了我對數學家工作內容的思考。
首先，我要坦白：我去參加這個分會場是因為我喜歡橙子。 第一個講座是托馬斯·黑爾斯的講座，他最出名的可能是他對開普勒猜想的證明。 簡而言之，該猜想認為，雜貨商堆疊橙子的方式確實是最有效的方式。 這個證明是一個漫長的逐個案例的窮舉，而黑爾斯對裁判報告說裁判“99％確定該證明是正確的”並不滿意。 因此，他做了任何*數學家都會做的事情：他花了十多年的時間來編寫和驗證該結果的正式計算機證明。 我參加這個講座是因為我覺得任何提到開普勒猜想的講座都有很小的機會為聽眾準備橙子。
關於支援科學新聞報道
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞報道 訂閱。 透過購買訂閱，您將幫助確保有關塑造我們當今世界的發現和想法的具有影響力的故事的未來。
黑爾斯的講座簡稱為“形式證明”。 這些不是使用呆板的語言編寫的證明，也不是寫出每個步驟的證明，而是可以輸入計算機並一直驗證到數學基礎（無論選擇哪個基礎）的證明。
黑爾斯在他的演講開始時舉了一些不太正式的證明的例子，首先是威廉·瑟斯頓的一段話，其中他使用了“細分和抖動”這個短語，這顯然不是描述數學的嚴謹方式。 （順便說一句，瑟斯頓也用橙子做數學。 他會要求學生剝橙子，以更好地理解二維和三維幾何。）
雖然我從未見過瑟斯頓，但我卻是他的眾多數學後裔之一。 他研究數學的方法，特別是他對直覺和想象力的強調，已經滲透到我擴充套件的數學家族的文化中，並對我思考數學的方式產生了很大的影響。 這就是為什麼對我來說，去參加一個不以直覺為主要重點的講座是如此令人耳目一新的原因。
黑爾斯當然不是暗示瑟斯頓是一位糟糕的數學家。 瑟斯頓只是他用作不太嚴謹的數學例子的第一位數學家。 幾張幻燈片之後，他提到了關於集合論的布林巴基著作。 是的，即使是那個形式數學的典範，榨乾了每一滴直覺，也並非真正充滿了形式證明。
黑爾斯的講座很好地概述了現有的形式證明程式、一些已被正式證明的數學結果（包括一些已知的結果），以及對該領域未來發展方向的良好介紹。 我對更多地瞭解QED宣言和FABSTRACTS特別感興趣，FABSTRACTS是一項將數學論文摘要形式化的服務，這比形式化整篇論文的目標更易於實現。
這次演講最有趣的時刻，至少對我而言，是聽眾中有人問及是否可以使用形式證明助手來驗證望月新一的abc猜想的證明。 黑爾斯回答說，以目前的技術，您確實需要在輸入證明時理解它，因此沒有多少人可以做到這一點。 合乎邏輯的回應是：為什麼望月新一自己不做呢？ 讓我們就說我不抱太大期望。
我參加的本分會場的第二個講座是邁克爾·舒爾曼的講座，名為“從nLab到HoTT書籍”。 他談到了nLab（一個範疇論的維基）和同倫型別論“研究教科書”的寫作，這是一本在IAS學期關於同倫型別論（一種替代集合論作為數學基礎系統的理論）期間編寫的600頁鉅著。 舒爾曼演講的主題是“一種尺寸並不適合所有”，無論是在人們協作的方式（對比維基和教科書）還是在數學的基礎（型別論與集合論）方面都是如此。
我不知道這是否是故意的，但我認為舒爾曼的演講是對黑爾斯演講的一個有趣的對比，對我來說最相關的是它回答了黑爾斯提出的一個問題：為什麼沒有更多的數學家使用證明助手？ 除了證明助手目前對我們許多人來說過於笨重之外，舒爾曼的回答是，我們進行數學是為了理解，而不僅僅是為了真理。 他說出了我在黑爾斯演講期間的想法，那就是對於許多數學家來說，使用形式證明助手“感覺不像”數學。 我在這裡不是在宣稱道德制高點。 實際上，對我來說，能夠更快地發現和驗證新真理的前景對我來說並沒有那麼重要，這有點令人驚訝。
你永遠不知道當你走進一個遠超出你的數學舒適區的講座時會得到什麼。 就我而言，我最終沒有得到任何橙子，但我獲得了一些關於我們如何以及為何證明的有趣的新視角。
*幾乎沒有