計算進化史：改變數學的命運

從古典時代說起，關於數學，美索不達米亞人選擇了計算，希臘由於沒有得到完整的傳承，機緣巧合之下選擇了推理，此後數學的公理化往往繞開計算，偏重證明，即數學論證偏於推理，然而數學實踐卻始終繞不開計算，特別是幾何公理化中難以解決的圖形面積問題，calculus這種演算法方法卻融入了幾何學的聖殿，致使17世紀之後的數學家能夠探索更廣闊的數學世界。

還是得提到公理問題，我們對公理的判定到底是分析還是綜合的呢？憑什麼我們要不加證明地接受公理呢？龐加萊提出的答案是：一個詞的含義就是與該詞相關的所有真命題的集合。

自龐加萊以後，我們就了解到，並不是因為我們知道了這些詞的含義，這條公理就奇蹟般地成了一個看似顯然的命題，而是因為公理恰恰是這些詞定義的一部分，我們才認為它成立。

這種對於定義的理解，解決了歐幾里得《幾何原本》中因定義「點」的概念而帶來的一個古老問題。歐幾里得對「點」的定義相當模糊：「點是沒有部分的東西。」然後，他提出了各種公理並證明了各種定理，卻從來沒有用到過「點」的定義。那麼這個定義到底是幹什麼用的呢？在龐加萊看來，這個定義根本沒有用——「點」這一概念的真正定義並不在這句含義不明的話里，而在於幾何的公理之中。

謂詞邏輯綜合了亞里士多德和斯多葛的邏輯，只要接受設置幾條公理，任何數學都可以用它表達。這一邏輯的建立對我們理解推理的本質而言是一大進步，大概是自古以來最重要的進展了。而澄清推理的本質，對推理與計算之間的關係具有深遠的影響。

謂詞邏輯對計算依然置之不理，然而此時歐幾里得演算法的地位改變了，它由單純地「算」公約數變成了可以判定「數 x 和數 y 的最大公約數是數 z 」這個命題的演算法！再這之後各種演算法開始準備取代「判定命題是否成立」的東西。

塔斯基演算法的野心還要更大，因為所有歐氏幾何問題都可以歸結為用加法和乘法表達的實數問題。塔斯基演算法的存在，意味著所有幾何問題都可以通過計算來解決。雖然古希臘人也引入了推理來解決問題，特別是幾何問題，但他們沒能達到用計算解決的高度。塔斯基卻證明了——至少對於幾何而言，當初從計算向推理的轉變毫無必要，因為古希臘人未能預見的這種新演算法可以代替推理。

20 世紀 20 年代，希爾伯特提出了一個問題，並稱之為「判定性問題」：有沒有一種演算法，能夠判定在謂詞邏輯下的命題是否可以證明成立呢？

希爾伯特提出讓計算回歸，並不完全出於實用的目的。弗雷格先前提出了一套自相矛盾的邏輯，可以同時證明某件事及其對立面。這促使羅素及隨後的希爾伯特對其加以了修正，他們由此得出的謂詞邏輯看起來沒有矛盾，因為當時還沒人能找到悖論。但希爾伯特也無法保證，他的邏輯不會早晚面臨像弗雷格邏輯一樣的命運：如果有人能夠同時證明某件事和它的對立面，那謂詞邏輯就算完蛋了。這才是希爾伯特用計算代替推理的主要原因——計算可以顯示某個命題為真或為假。這樣一來，演算法絕不會同時得出兩個不同的結論，那麼從構造上就保證了這個邏輯不會有矛盾。

1936 年，阿隆佐·丘奇和阿蘭·圖靈分別獨立解決了判定性問題，其答案是否定的：謂詞邏輯不存在一種判定性演算法。20世紀30年代的數學家們給出了若干不同的定義：法國數學家雅克·埃爾布朗和庫爾特·哥德爾提出了「埃爾布朗–哥德爾方程組」，丘奇提出了「λ演算」，圖靈提出了「圖靈機」，斯蒂芬·科爾·克萊尼則提出了「遞歸函數」……

由此，計算更接近推理了，最終人們認為計算規則和演繹規則之間的區別就是可以停下來。眾所周知，停機問題被證明為不可解，證明了某些問題無法用計算解決，這也證明了從全由演算法構成的史前數學過渡到古希臘數學是完全必要的。

所以停機問題說明：不存在判定一個謂詞邏輯命題是否可證明的演算法。——丘奇定理

這也給數學家們掙回來了臉面，畢竟謂詞邏輯說數學都是分析判斷，都是很顯然的，很是打數學家們的臉啊，如果真理是顯然的，那就應該存在一個演算法，能告訴我們從一組公理中可以得出哪些結論，但丘奇定理恰恰證明了事實並非如此。分析並非顯然。

將「可計算」與「分析」混為一談，這種錯誤在自然科學的數學化討論中十分常見。力學已經在17世紀數學化了，也就是說，力學變成了一套公理化理論。於是我們有時候就會聽人們說，解決一個力學問題（比如計算某個行星在未來某天所處的位置）無非是簡單算一下就好了。這種論調違背了丘奇定理——力學一旦完成了數學化，解決問題需要的就不是計算，而是推理。

世界是複雜的呢。

丘奇論題認定了下面這兩個概念其實是一回事：由λ演算和圖靈機等定義的「計算」概念，以及「通用」的計算概念。

事實上，要明確演算法的概念有兩種辦法，取決於計算是由數學家來做，還是由一個物理系統（一台機器）來做。這就把丘奇論題的兩種變形區分開來，我們可以稱之為丘奇論題的「心理」形式和「物理」形式。丘奇論題的心理形式指的是：人類為解決某一特定問題所能完成的所有演算法，都可以用一組計算規則來表達。其物理形式則說的是：物理系統（機器）為解決某一特定問題所能系統執行的所有演算法，都可以用一組計算規則來表達。

額，這裡我已經看不懂了，因為想要反駁這兩個論題需要藉助心理學與物理學原理，羅賓-甘迪給出了物理形式證明，但是他給出的兩個假設依然需要驗證。

自然法則可以數學化是丘奇論題的一個結論

依然難以看懂。

λ演算與β歸約

λ演算試圖讓計算佔有一席之地，它接近於函數，替換變數過程被稱為β歸約，Church認為λ演算也就是計算，在其與圖靈機的證明等價後，這被認為是對的。然而，它在作用於自身上，依然產生矛盾，幾經波折，這條路還是失敗了，可計算性理論還是失敗了，證明仍然是基於謂詞邏輯的證明，由公理和演繹規則構建而成，並符合數學的公理化思想。而且在這些證明中，並未給計算留下一絲一毫的位置。

可計算性理論失敗了，我們看看可構造性理論，一個非常簡單的例子

如果一個集合包含數字 1 但不包含數字 3，那麼肯定存在一個數字 n，使得該集合包含數字 n 卻不包含 n+1。因為要麼數字 2 在集合里，那麼答案就是 2；要麼不在集合里，答案就是 1。

非構造性證明中無法找出例證，我們只能使用排中律，構造主義開始拒絕在數學中使用排中律，當然最終他們還是銷聲匿跡了，但是構造主義危機使得人們注意到了「存在」的不尋常性。

我們已經看到，使用排中律的存在性證明不一定會給出例證。相反，不使用排中律的存在性證明則似乎總是包含一個例證，無論是以顯式還是隱式的方式給出。我們能不能從這種印象入手，證明它總是如此呢？

1935年切消演算法被提出，它直接作用於證明，使我們明白「不使用排中律的存在性證明必然包含一個例證，至少是隱含其中。」由此，演算法的概念獲得了一種更為抽象的全新定義：演算法是可以用構造性方式定義的函數。

演算法解釋」主要還是在 20 世紀 60 年代由哈斯凱爾·柯里、荷蘭數學家尼古拉斯·霍弗特·德布魯因和美國數學家威廉·阿文·霍華德等人發展完善的。

證明的演算法解釋推翻了自歐幾里得以來，一直將數學建立在證明概念上的公理化方法觀點。人們由此發現，證明的概念並不是一個原始概念，它可以用更基礎的概念——演算法來定義。總之，美索不達米亞人將所有的數學都構建在演算法之上，在不知不覺中選擇了最根本的概念。古希臘人將數學構建在證明之上，則是造成了一個扭曲的印象。

然而構造性理論還是得出了一個悖論，它仍然沒有對公理化思想提出質疑，在接下來的 10 年間，批判公理化方法的變革終於爆發了。

公理化危機

在直覺主義類型論之後，自動化證明開始興起，即使停機問題不可解，但是程序依然可以只去尋找證明

第一個問題：在理論上，機器做證明有沒有可能像人類做得那麼好？如果我們接受了丘奇論題的心理形式，那麼似乎至少從理論上，人類做證明的思維過程可以用一套計算規則來模擬，因此也就可以用計算機來模擬。由於丘奇論題的心理形式只是一個假說，那麼它的對立面也有可能成立，即人類和機器之間有一道不可逾越的屏障，人類永遠都比機器更善於做證明。然而，要支持後面這種說法就必須否定丘奇論題的心理形式，而我們在前面已經看到，丘奇論題的心理形式是另外兩個論題的結果：丘奇論題的物理形式，以及唯物主義論題，即人類是自然的一部分。這樣一來，就至少得否定這兩個論題中的一個：要麼否定「人類是自然一部分」，那就意味著否定精神是大腦機能的產物；要麼否定丘奇論題的物理形式，這又導致要麼否定信息密度有限，要麼否定信息傳播的速度有限。當然，羅傑·彭羅斯等人希望有一種新的物理學，能夠挑戰信息密度有限和信息傳播速度有限的定律，並由此解釋計算機為什麼不能模擬大腦的機能。

第二個問題與第一個問題相對獨立：在現有的條件下，機器有沒有可能把證明做得和人類一樣好？這個問題就比較容易回答了：就算我們認為機器在理論上可以和人類一樣善於做證明，也不得不承認現有的自動化證明程序還是不如人類。

最後一個問題：如果機器做證明的能力和人類一樣強，我們有沒有理由害怕機器呢？首先，就算這種恐懼有道理，它也不影響前兩個問題的答案。假如僅僅因為我們不情願承認，就說機器不可能比人類更善於做證明，那這和因為厭惡而謊稱砒霜沒有毒一樣荒謬。讓我們回到這個問題本身：誠然，我們很難說清這種恐懼到底有沒有道理，但機器在做乘法、下象棋和搬重物方面已經「勝過」人類，而這些機器並沒有奪權。那麼，我們還有理由擔心機器比人類更擅長做證明嗎？

需要直接引用的一段文字。但是自動化證明並不能做到一切。所以人們由讓機器完全取代的觀念已經轉變為讓機器與人類合作，人類來做證明，機器來驗證其中細小的錯誤。所以，為了構建證明，不但要使用公理和演繹規則，還要使用計算規則。

四色定理成了第一個敘述簡短而證明極度冗長的定理。而且迄今為止也沒有找到短證明。丘奇定理有這樣一個結論：存在這樣的定理，其長度是 n，而其最短的證明至少長達 1000n，或者甚至是 2^n。

由此看來，證明命題的難度分為幾個等級：

• 有些命題有短的公理性證明；

• 有些命題沒有短的公理性證明，但採用計算之後有短證明；

• 有些命題就算用上了計算，也還是只有長證明。

後面的一章 工具 提到不尋常的一點，數學家使用的工具與任何其他科學家都不同，他們的工具是平凡的，根據丘奇定理，人類或機器所能完成的所有運算都可以用一組計算規則來表達，從而用商用計算機來完成。不過這種解釋並不完整。這得用到一部分經濟學原理。

在自動化證明乃至切消理論中，公理的存在是許多困難的根源。公理已經「污染」了自希爾伯特以來的數學。希爾伯特希望將人們從公理和演繹規則中解放出來，但這個目標太大，最終失敗了。然而，如果能夠擺脫公理而保留演繹規則，那也算是一個重大進步了。

是否有那麼一天，計算能讓我們掙脫公理的束縛？還是說，就算有了計算，我們仍然必須在數學大廈中給公理留有一席之地呢？

這本書講的是計算的進化史，由於內容本身的巨大信息量，這200多頁也只能簡要講述一下各種思想的來源與結論，鑒於分析的複雜性，於我而言，還有許多內容得找大量的原始資料才能看懂。

我對這段漫長歷史的感受是：沒有什麼是必然存在的，即使公理也不能端坐寶位不下台，如果一切都要受到檢驗，那麼公理化也並非萬能，我們建立的地基也不過是普通的材料構成而已，看似輝煌，難保哪天就會倒塌，在越來越多只有長證明的命題出現，以人類的精力已經不可能完成。計算必將深入數學，甚至取代公理與演繹規則，公理的神聖性消亡了。

最近恰逢柯潔與AlphaGo的人機大戰，人類三場全敗。有幾點感悟

• 圍棋的「文化」被機器擊潰了，圍棋高手再也沒有了那些「智慧」光環，以丘奇論題來說，我們不能保證人類計算就要比計算機這個物理系統更加完備，人類主義要不得。
• 人工智慧再次向我們展示計算的威力，畢竟四色定理直到今天還是由計算機才能做出，抱著古希臘證明為數學之基這種觀念是沒必要的，公理與證明的神聖性被打破了
• 我們走在計算的進化史之路上，目的不是為了繞來繞去的邏輯和讓計算機替我們幹活這種初級的事兒，在探索真理的過程中，我們想要知道有什麼是不可代替的，希臘文明選擇的數學之路難道就是完全正確的嗎？直到微積分發明之前，連計算面積這種問題都能阻礙先驅之路，我們有什麼理由鄙夷計算呢？我們何以自豪與我們粗陋的「推理」？

寫到結尾時隨機到的一首音樂，前進吧！但不要抱著人類主義。