原標(biāo)題：Voevodsky | 單一基礎(chǔ)的源起——為避免數(shù)學(xué)錯(cuò)誤而發(fā)展計(jì)算機(jī)驗(yàn)證證明的個(gè)人使命

作者 |Vladimir Voevodsky

譯者 |鄧文超，中國科學(xué)院大學(xué)基礎(chǔ)數(shù)學(xué)碩士研究生。

Vladimir Voevodsky 在 2002 年作為教授加入 IAS數(shù)學(xué)系，他因在概型的同倫理論，代數(shù) K 理論和代數(shù)幾何與代數(shù)拓?fù)浣徊娌糠值墓ぷ鞫Ｋ麑?duì)代數(shù)簇發(fā)展了新的上同調(diào)理論，這是過去幾十年來代數(shù)幾何最突出的進(jìn)展。他的工作直接導(dǎo)致了 Milnor 猜想和 Bloch-Kato 猜想的解決。

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

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

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

接著，我們想可以將相似的想法應(yīng)用到另一個(gè)那時(shí)的頂尖數(shù)學(xué)難題：構(gòu)造 motivic 上同調(diào)，Alexander Beilinson, Robert MacPherson(現(xiàn)在是IAS的數(shù)學(xué)系教授) 和 Vadim Schechtman 在 1987 年合作的一篇論文中猜想這個(gè)數(shù)學(xué)對(duì)象是存在的。

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

motivic 上同調(diào)在那時(shí)被認(rèn)為僅僅是個(gè)猜測(cè)，還缺乏堅(jiān)實(shí)的基礎(chǔ)。Spencer Bloch 在 1986 年的突破性論文《代數(shù)循環(huán)和高階 K 理論》(Algebraic Cycles and Higher K-theory)也很快被 Andrei Suslin 發(fā)現(xiàn)在引理 1.1 的證明中包含一個(gè)錯(cuò)誤。這個(gè)證明無法被修復(fù)，于是論文中的幾乎所有論斷都無法被證明。

一個(gè)新的證明直到 1993 年才公布，這個(gè)新證明用 30 頁的復(fù)雜討論替換原來論文中的一段。有趣的是，這個(gè)新的證明是基于 Mark Spivakovsky 的一個(gè)舊有的結(jié)果。Mark Spivakovshy 在那時(shí)也宣布了奇點(diǎn)消解猜想的證明。不過，Spivakovshy 的證明在多年后被發(fā)現(xiàn)包含一個(gè)錯(cuò)誤，所以奇點(diǎn)消解猜想現(xiàn)在仍是公開問題。

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

這段故事讓我覺得后怕。從 1993 年開始，很多數(shù)學(xué)家群體在討論班上研究了我的論文，并將其應(yīng)用到他們的工作之中，但是沒有人注意到這個(gè)錯(cuò)誤。這當(dāng)然不是一個(gè)容易避免的事情。因?yàn)檫@個(gè)由一位被信任的作者給出的技術(shù)性討論本身就感覺像是正確的而不容易被很細(xì)心地檢查出來。

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

我發(fā)現(xiàn)導(dǎo)致這種反常情況出現(xiàn)的兩個(gè)因素：Simpson 聲稱構(gòu)造出了一個(gè)反例，但是他沒有找出我們論文中的錯(cuò)誤。故而，我們并不清楚到底是我們論文中有錯(cuò)誤還是他在構(gòu)造反例的時(shí)候出了錯(cuò)。現(xiàn)在的數(shù)學(xué)研究依賴一個(gè)基于數(shù)學(xué)聲譽(yù)的復(fù)雜互信系統(tǒng)。Simpson 的論文出現(xiàn)的那時(shí)，Kapranov 和我都有很好的數(shù)學(xué)聲譽(yù)。Simpson 的論文對(duì)我們的結(jié)果產(chǎn)生了懷疑，這導(dǎo)致它不被其他研究者使用，但是沒有人繼續(xù)前進(jìn)并向我們?cè)谶@個(gè)問題上提出異議。

在我發(fā)現(xiàn)我的 motivic 上同調(diào)論文中的錯(cuò)誤時(shí)，我正在發(fā)展新的理論，我稱之為 2-理論。在我考慮這些想法的時(shí)候，我越來越不確定應(yīng)該怎么推進(jìn)。2-理論的數(shù)學(xué)正是 Kapranov 和我在 1989 年夢(mèng)想的那種高維數(shù)學(xué)。我非常享受發(fā)現(xiàn)了并不是低維結(jié)構(gòu)直接推廣的新的高維結(jié)構(gòu)。

但是想要達(dá)到我覺得必要的那種嚴(yán)格和精確程度需要花費(fèi)大量的精力，并且會(huì)產(chǎn)生一篇很難閱讀的論文。誰能保證我不會(huì)忘掉什么或者犯個(gè)什么錯(cuò)誤呢，甚至某個(gè)很簡單的論證中的錯(cuò)誤都有可能在多年后才被發(fā)現(xiàn)。我想正是在這個(gè)時(shí)候，我停止了去做那種“好奇心驅(qū)動(dòng)型研究”，轉(zhuǎn)而開始嚴(yán)肅地考慮未來。我并沒有能探索好奇心帶領(lǐng)到達(dá)的有價(jià)值的、有趣的并且很優(yōu)美地方的工具。

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

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

Tom Hales 和 Carlos Simpson 是那時(shí)堅(jiān)持嘗試發(fā)展數(shù)學(xué)中的機(jī)器驗(yàn)證的少數(shù)數(shù)學(xué)家。幾年后的現(xiàn)在，證明和數(shù)學(xué)推理的機(jī)器驗(yàn)證對(duì)許多工作在單一基礎(chǔ)(univalent foundations)和同倫型理論(homotopy type theory)領(lǐng)域的數(shù)學(xué)家來說，基本上看起來完全可行了。

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

不過，要接受數(shù)學(xué)需要一個(gè)全新的基礎(chǔ)這一觀點(diǎn)仍然是十分困難的。即使很多直接接觸同倫型理論的人也不容易接受這個(gè)想法。一個(gè)原因是：現(xiàn)有的數(shù)學(xué)基礎(chǔ)——ZFC 和范疇論——已經(jīng)十分成功。我很傾向于用范疇論作為新的數(shù)學(xué)基礎(chǔ)。

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

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

對(duì)我來說最大的路障就是這個(gè)“范疇是下一個(gè)維度中的集合”。我清楚地記得我明白這個(gè)觀點(diǎn)是錯(cuò)誤的的時(shí)候的感覺。范疇不是“下一個(gè)維度中的集合”，他們是“下一個(gè)維度中的偏序集”，而“下一個(gè)維度中的集合”是廣群。

這種“廣群”和“范疇”的新看法對(duì)我來說需要一些調(diào)整，我記得教我數(shù)學(xué)的人們強(qiáng)調(diào)過一件事: Grothendieck 處理代數(shù)幾何的方法會(huì)如此成功的一個(gè)原因就是他和舊有的做法決裂了，他堅(jiān)持認(rèn)為考慮所有的態(tài)射而不僅僅是同構(gòu)是重要的。(廣群經(jīng)常是由集合級(jí)別的對(duì)象和它們之間的同構(gòu)造出來的，而范疇常是由集合級(jí)別的對(duì)象和所有的態(tài)射造出來的。)

單一基礎(chǔ)是一個(gè)完備的基礎(chǔ)系統(tǒng)，相比范疇論，它更像 ZFC，但它和 ZFC 是非常不同的。為了作比較，我假設(shè)任何既適合人類推理又適合計(jì)算機(jī)驗(yàn)證的的數(shù)學(xué)基礎(chǔ)應(yīng)該包含下面這三個(gè)部分。

第一部分是形式推導(dǎo)系統(tǒng)：包括一種語言和用這種語言操作純粹形式化語句的規(guī)則，使得這些操作可以被計(jì)算機(jī)程序檢驗(yàn)。第二部分是一個(gè)結(jié)構(gòu)，這個(gè)結(jié)構(gòu)要能對(duì)這種語言中的語句給出人類頭腦可直覺感知的對(duì)象。第三部分是另一個(gè)結(jié)構(gòu)，這個(gè)結(jié)構(gòu)幫助人們理解直接與這種語言相聯(lián)系的數(shù)學(xué)想法。

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

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

單一基礎(chǔ)的第二組成部分，給 CIC 的語句提供直接含義的結(jié)構(gòu)是基于單一模型的。直接與 CIC 的語句相聯(lián)系的對(duì)象被稱之為同倫型。同倫型的世界是被我們稱之為 h-級(jí)的東西分層的，1 h-級(jí)的型對(duì)應(yīng)命題，2 h-級(jí)的型對(duì)應(yīng)集合。我們關(guān)于高階級(jí)的直覺大部分來自它們和高維形狀的關(guān)系，這些是基于 ZFC 的數(shù)學(xué)考慮了幾十年的事情。

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

我從 2005 年開始到現(xiàn)在就一直在考慮這些引導(dǎo)發(fā)現(xiàn)單一模型的想法，并且于 2009 年 11 月在 Ludwig-Maximilians-Universit?t München 做了關(guān)于此主題的第一個(gè)公開報(bào)告。當(dāng)我獨(dú)立構(gòu)建模型的時(shí)候，這個(gè)方向的一些進(jìn)展從 1995 年就開始了，主要是 Martin Hofmann, Thomas Streicher, SteveAwodey, 和 Michael Warren 在做。

我在 2010 年春天向 IAS 數(shù)學(xué)系建議在 2012-2013 年組織一個(gè)關(guān)于新的數(shù)學(xué)基礎(chǔ)的特殊項(xiàng)目，盡管在那時(shí)仍然不清楚這個(gè)領(lǐng)域是否準(zhǔn)備好這樣一次研討。

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

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

推薦參考：Vladimir Voevodsky 于 2012-2013 年在研究院組織的關(guān)于單一基礎(chǔ)的特殊項(xiàng)目里二十多位數(shù)學(xué)家一起在六個(gè)月內(nèi)寫了一本六百多頁的參考書。這本書可從 http://suo.im/5ikLSg 免費(fèi)獲取。這篇文章來自 Voevodsky 在三月份的一個(gè)報(bào)告，當(dāng)時(shí)的錄像可在 http://suo.im/4GJfAm 查看。返回搜狐，查看更多

責(zé)任編輯：

總結(jié)

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

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。