原標題：Voevodsky | 單一基礎的源起——為避免數學錯誤而發展計算機驗證證明的個人使命

作者 |Vladimir Voevodsky

譯者 |鄧文超，中國科學院大學基礎數學碩士研究生。

Vladimir Voevodsky 在 2002 年作為教授加入 IAS數學系，他因在概型的同倫理論，代數 K 理論和代數幾何與代數拓撲交叉部分的工作而知名。他對代數簇發展了新的上同調理論，這是過去幾十年來代數幾何最突出的進展。他的工作直接導致了 Milnor 猜想和 Bloch-Kato 猜想的解決。

圖 1: 這個三維圖表是 Veovodsky 用來支持他關于 2-理論的論證所用“公式”的一個例子

Alexander Grothendieck 在 1984 年 1 月向法國國家科學研究中心提交了他的項目申請書“Esquisse d’un Programme”。這份文稿很快就在數學圈里傳閱。幾個月后，我的第一位學術研究導師 George Shabat 也給了我一份，當時我是莫斯科大學的一年級本科生。為了讀它，我專門學了一些法語，之后我開始閱讀并努力理解其中的想法。

我在1988 或1989 年遇到了 Michael Kapranov, 他也對發展數學中新的“高維”對象的想法極感興趣，這些想法來自范疇和 2-范疇理論的啟發。我們合作發表的第一篇論文是《無窮廣群是同倫范疇的一個模型》(-Groupoids as a Model for a Homotopy Category)。在文中，我們想要提供一個嚴格的數學形式化和對 Grothendieck的某個想法的證明，Grothendieck的這個想法意圖聯系 -廣群和同倫型這兩類數學對象。

接著，我們想可以將相似的想法應用到另一個那時的頂尖數學難題：構造 motivic 上同調，Alexander Beilinson, Robert MacPherson(現在是IAS的數學系教授) 和 Vadim Schechtman 在 1987 年合作的一篇論文中猜想這個數學對象是存在的。

Kapranov 在 1990 年夏天安排我免申請進入哈佛大學研究生院。幾個月之后，他在康奈爾，我在哈佛，我們的數學道路有了分歧。我集中精力于 motivic 上同調和后來的 motivic 同倫論。1991 年 3 月 29 日我的筆記開頭是一個問題：“什么是代數簇或概型的同倫論？”

motivic 上同調在那時被認為僅僅是個猜測，還缺乏堅實的基礎。Spencer Bloch 在 1986 年的突破性論文《代數循環和高階 K 理論》(Algebraic Cycles and Higher K-theory)也很快被 Andrei Suslin 發現在引理 1.1 的證明中包含一個錯誤。這個證明無法被修復，于是論文中的幾乎所有論斷都無法被證明。

一個新的證明直到 1993 年才公布，這個新證明用 30 頁的復雜討論替換原來論文中的一段。有趣的是，這個新的證明是基于 Mark Spivakovsky 的一個舊有的結果。Mark Spivakovshy 在那時也宣布了奇點消解猜想的證明。不過，Spivakovshy 的證明在多年后被發現包含一個錯誤，所以奇點消解猜想現在仍是公開問題。

我、Andrei Suslin 和 Eric Friedlander 發展的通往 motivic 上同調的路徑通過我的論文《帶有轉移的預層的上同調理論》“Cohomological Theory of Presheaves with Transfers”回避了 Bloch 的那個引理，這篇論文是我作為IAS成員時在 1992-1993 年完成的。1999-2000 年，同樣是在 IAS，我給了一個系列講座，PierreDeligne(IAS數學系教授)當時在做筆記并檢查我的每一個步驟。正是這樣，我發現論文中的一個關鍵引理的證明包含一個錯誤，并且這個錯誤無法修補。幸運的是，我后來證明了一個稍弱但更復雜的引理，這個引理對論文中的應用是充分的。于是，在 2006 年，正確的論證發表了出來。

這段故事讓我覺得后怕。從 1993 年開始，很多數學家群體在討論班上研究了我的論文，并將其應用到他們的工作之中，但是沒有人注意到這個錯誤。這當然不是一個容易避免的事情。因為這個由一位被信任的作者給出的技術性討論本身就感覺像是正確的而不容易被很細心地檢查出來。

但是這并不是數學文本中的錯誤一直存在的唯一問題。1998 年 10 月，Carlos Simpson 向 arXiv 預印本文庫提交了一篇論文——《嚴格3-廣群的同倫型》(Homotopy Types of Strict 3-groupoids)。這篇論文中的論證表明 Kapranov 和我在 1989 年發表的那篇關于“ -廣群”的論文中的主要結果是不正確的。然而，Kapranov 和我也曾想過類似的批評，并且相信這樣的批評不成立。一直到 2013 年的秋天，我才確定我們倆是正確的。

我發現導致這種反常情況出現的兩個因素：Simpson 聲稱構造出了一個反例，但是他沒有找出我們論文中的錯誤。故而，我們并不清楚到底是我們論文中有錯誤還是他在構造反例的時候出了錯。現在的數學研究依賴一個基于數學聲譽的復雜互信系統。Simpson 的論文出現的那時，Kapranov 和我都有很好的數學聲譽。Simpson 的論文對我們的結果產生了懷疑，這導致它不被其他研究者使用，但是沒有人繼續前進并向我們在這個問題上提出異議。

在我發現我的 motivic 上同調論文中的錯誤時，我正在發展新的理論，我稱之為 2-理論。在我考慮這些想法的時候，我越來越不確定應該怎么推進。2-理論的數學正是 Kapranov 和我在 1989 年夢想的那種高維數學。我非常享受發現了并不是低維結構直接推廣的新的高維結構。

但是想要達到我覺得必要的那種嚴格和精確程度需要花費大量的精力，并且會產生一篇很難閱讀的論文。誰能保證我不會忘掉什么或者犯個什么錯誤呢，甚至某個很簡單的論證中的錯誤都有可能在多年后才被發現。我想正是在這個時候，我停止了去做那種“好奇心驅動型研究”，轉而開始嚴肅地考慮未來。我并沒有能探索好奇心帶領到達的有價值的、有趣的并且很優美地方的工具。

所以，我開始考慮我能不能造出這樣的工具。很快我就明白解決的途徑就是用計算機去驗證我的那些抽象的、邏輯的和數學的構造。這樣的軟件從六十年代起就在發展。但當我在 2000 年左右尋找這樣一個實用的證明輔助軟件時，我并沒有找到。有好幾個課題組在做這樣的軟件，但沒有一個符合我那種數學的需求。

當我第一次開始探索這種可能性的時候，機器驗證證明還幾乎是一個在數學家群體里被禁止的主題。對機器驗證證明的討論無疑會導向 G?del 不完備性定理(這個定理對實際問題沒有任何用處)或者有一兩個例子對已有的證明進行了驗證，這只能表明機器驗證證明這個想法的不實用性。

Tom Hales 和 Carlos Simpson 是那時堅持嘗試發展數學中的機器驗證的少數數學家。幾年后的現在，證明和數學推理的機器驗證對許多工作在單一基礎(univalent foundations)和同倫型理論(homotopy type theory)領域的數學家來說，基本上看起來完全可行了。

最核心的待解決的挑戰是現有的數學基礎達不到做這件事的要求。用一種足夠精確使得計算機可以理解的語言形成數學推理意味著不僅將使用數學的基礎系統作為建立一些基本定理的一致性準則，還將其作為一個可以被使用到日常數學工作中的工具。現有的基礎系統主要有兩個導致其不合乎需要的問題。第一，現有的數學基礎是基于謂詞邏輯的語言，但是這種類型的語言限制性太大。第二，現有的基礎不能被用來直接表達有些對象，比如我在 2-理論工作中的某些對象。

不過，要接受數學需要一個全新的基礎這一觀點仍然是十分困難的。即使很多直接接觸同倫型理論的人也不容易接受這個想法。一個原因是：現有的數學基礎——ZFC 和范疇論——已經十分成功。我很傾向于用范疇論作為新的數學基礎。

故事從 ZFC 開始：Zermelo-Fraenkel 理論和選擇公理。從二十世紀的前半葉開始，數學就成為一個基于 ZFC 的科學，ZFC 是作為謂詞邏輯中的一個特殊理論引進的。所以，想要接觸數學底層的人有一條簡單的路——學習什么是謂詞邏輯，然后學習一種叫做 ZFC 的特殊理論，然后學習如何將涉及一些基本數學概念的命題翻譯成 ZFC 中的公式，然后通過例子學習去相信其余的數學都可以化約到這些基本的概念。

這種情形對數學是十分有益的，正是它促成了二十世紀抽象數學的成功。歷史上，ZFC 的第一個問題從早期布爾巴基宏偉事業的衰落中就可以看到，這個衰落是由于二十世紀后半葉的中心方法是范疇論，但是范疇論在 ZFC 框架里不太好表達。范疇論的成功使得人們覺得范疇是“下一個維度中的集合”，數學的基礎應該是范疇論或者它的高維類似物。

對我來說最大的路障就是這個“范疇是下一個維度中的集合”。我清楚地記得我明白這個觀點是錯誤的的時候的感覺。范疇不是“下一個維度中的集合”，他們是“下一個維度中的偏序集”，而“下一個維度中的集合”是廣群。

這種“廣群”和“范疇”的新看法對我來說需要一些調整，我記得教我數學的人們強調過一件事: Grothendieck 處理代數幾何的方法會如此成功的一個原因就是他和舊有的做法決裂了，他堅持認為考慮所有的態射而不僅僅是同構是重要的。(廣群經常是由集合級別的對象和它們之間的同構造出來的，而范疇常是由集合級別的對象和所有的態射造出來的。)

單一基礎是一個完備的基礎系統，相比范疇論，它更像 ZFC，但它和 ZFC 是非常不同的。為了作比較，我假設任何既適合人類推理又適合計算機驗證的的數學基礎應該包含下面這三個部分。

第一部分是形式推導系統：包括一種語言和用這種語言操作純粹形式化語句的規則，使得這些操作可以被計算機程序檢驗。第二部分是一個結構，這個結構要能對這種語言中的語句給出人類頭腦可直覺感知的對象。第三部分是另一個結構，這個結構幫助人們理解直接與這種語言相聯系的數學想法。

在基于 ZFC 的數學基礎中，第一組成部分有兩“層”。第一層是建立推理系統的通用機制，叫做謂詞邏輯；第二層是叫做 ZFC 的具體的推理系統，這是通過將通用機制應用到一些操作和公理上得到的。ZFC 的第二組成部分是基于人類自然感知層次體系的能力。實際上，ZFC 公理可以看作是所有層次體系滿足的性質，再加上無窮公理，而無窮公理就是假定無窮層次體系是存在的。第三組成部分是根據層次體系翻譯數學概念，這些層次體系開始于集合的數學性質的編制規則。這就是 ZFC 經常被稱為集合論的原因。

單一基礎最初的形式演繹系統叫做歸納構造演算，即 CIC(calculus of inductive construction)。這是 Thierry Coquand 和 Christine Pauline 在大約 1988 年發展的，是基于計算機語言理論和實踐里的想法以及構造數學里的想法。這些想法的主要貢獻者有 Nicolaas Govert de Bruijn, Per Martin-L?f 和Jean-Yves Girard。證明輔助形式演繹系統 Coq 就是 CIC 的一個直接產物。

單一基礎的第二組成部分，給 CIC 的語句提供直接含義的結構是基于單一模型的。直接與 CIC 的語句相聯系的對象被稱之為同倫型。同倫型的世界是被我們稱之為 h-級的東西分層的，1 h-級的型對應命題，2 h-級的型對應集合。我們關于高階級的直覺大部分來自它們和高維形狀的關系，這些是基于 ZFC 的數學考慮了幾十年的事情。

單一基礎的第三組成部分，用同倫型翻譯一般數學概念的途徑，是基于 Grothendieck 在 70 年代后期的想法的反向考慮，這在我們的“ -廣群”論文中進行過討論。不論從數學上還是哲學上來講，這塊都是該理論最深和最少被理解的部分。

我從 2005 年開始到現在就一直在考慮這些引導發現單一模型的想法，并且于 2009 年 11 月在 Ludwig-Maximilians-Universit?t München 做了關于此主題的第一個公開報告。當我獨立構建模型的時候，這個方向的一些進展從 1995 年就開始了，主要是 Martin Hofmann, Thomas Streicher, SteveAwodey, 和 Michael Warren 在做。

我在 2010 年春天向 IAS 數學系建議在 2012-2013 年組織一個關于新的數學基礎的特殊項目，盡管在那時仍然不清楚這個領域是否準備好這樣一次研討。

現在我已經可以在我的證明輔助的幫助下做數學了。雖然這個證明輔助還有待完善，但至少我現在不用擔心所做數學工作中會包含錯誤了。現在做數學時，我能知道我真的做了什么，不用反復檢查，也不用擔心我的討論是否太過復雜，也不用擔心如何說服別人相信我的論證是正確的。我只需要相信計算機就好。現在有很多計算機科學的人在參與我們的項目，但是大部分數學家仍然不相信這是一個好想法，我覺得這是很不正確的。

感謝所有嘗試去理解單一基礎，發展這些想法和與別人交流這些想法的人們。

推薦參考：Vladimir Voevodsky 于 2012-2013 年在研究院組織的關于單一基礎的特殊項目里二十多位數學家一起在六個月內寫了一本六百多頁的參考書。這本書可從 http://suo.im/5ikLSg 免費獲取。這篇文章來自 Voevodsky 在三月份的一個報告，當時的錄像可在 http://suo.im/4GJfAm 查看。返回搜狐，查看更多

責任編輯：

總結

以上是生活随笔為你收集整理的错误源计算机检,Voevodsky | 单一基础的源起——为避免数学错误而发展计算机验证证明的个人使命...的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。