數學證明最早源於古希臘。他們發明（發現）了公理與邏輯，他們用證明來說服對方，而不是靠權威。這是徹頭徹尾的「去中心化」。自古希臘以降，這種方法論影響了整個人類文明的程序。
上圖是「勾股定理」的巧妙證明。歷史上曾出現過許許多多精巧的證明，神奇的思路，天才的靈感。一旦一個命題被證明，上帝都無能為力。嗯，對了，還有那個「上帝不是萬能的」證明：上帝不能造出一塊他舉不起來的石頭。
一個數學證明往往暗藏無比深刻的「洞見」，相信很多人都看過「費馬大定理」的故事[1]，這個定理證明橫跨四百年，從費馬寫下「這裡空間太小，我寫不下」，到懷爾斯最終登頂，耗費了許多代人的聰明才智。最近如「彭加萊猜想」，稍微帶點年代感的如「哥德巴赫猜想」，還有我非常敬佩的華裔科學家張益唐十年磨一劍，在仔細研究了「Goldston-Pintz-Yıldırım」和 「Bombieri-Friedlander-Iwaniec.」的證明「洞見」之後，證明了「質數間的有界間隔」[2]。
自十七世紀，萊布尼茨起，人們就夢想找到一種機械的手段，可以來自動完成證明，而不再依賴天才的靈光一現。
二十世紀初：「證明」 == 「符號推理」
時間到了十九世紀末，康託、布林、弗雷格、希爾伯特、羅素、布勞威、哥德爾等人定義了形式化邏輯的符號系統。而「證明」則是在利用形式化邏輯的符號語言編寫的推理過程。邏輯本身靠譜麼？邏輯本身「自恰」嗎？邏輯推理本身對不對，能夠證明嗎？這讓 數學家/邏輯學家/電腦科學家 發明（發現） 了符號系統，語法 vs. 語義，可靠 vs. 完備，遞迴 vs. 無窮。（這部分精彩故事請參看『邏輯的引擎』一書[3]）。
1910年，羅素髮表了洪(zhuan)荒(tou)鉅著『數學原理』。在書中，羅素與懷特海試圖將數學完整地「形式化」下來。如果能達到這樣的目標，所有的數學成果都將以證明的方式建立在堅實的基礎上。下圖就是『數學原理（卷二）』中的一頁：
其中110.643這是一個命題：「1+1=2」，然後接下來就是這個定理的證明。大家可能奇怪，難道 1+1 還需要證明嗎？是的，在數學原理一書中，數字 0，1，2，…… 都有嚴格定義，「加法」、「乘法」、「等於」都要嚴格定義，然後每一步的推理都需要指出依據。證明意味著什麼？證明是可能繁瑣無比的、但是每一步推理都嚴格無誤。書中大量的證明都機械式的，按照公理和推理規則進行一種證明的構造，尋找證明就好像可以交給一個人，然後他無腦在公理與推理規則的集合中進行機械查詢。
似乎人們距離「定理的自動證明」並不遙遠了。
不幸的是，哥德爾在 1931 年證明了「哥德爾不完備性定理」[4]，圖靈在 1936 年證明了圖靈機停機問題的不可判定性[5]。這些成果徹底終結了這個幾百年的幻想。無論公理系統如何精巧設計，都無法抓住所有的真理。
證明不僅僅是一個嚴格推理，而且凝結了似乎很難機械化的創造性思維。證明中蘊含了大量的「知識」，每一次的突破，都將我們的認知提升到一個新的高度。不管是「洞見」，還是推理過程中所構造的「演算法」，一個定理的證明的內涵往往遠超出定理本身的結論。
六十年代：「證明」 == 「程式」
又過了半個世紀，到了六十年代，邏輯學家 Haskell Curry 和 William Howard 相繼發現了在「邏輯系統」和「計算系統— Lambda 演算」中出現了很多「神奇的對應」，這就是後來被命名的「Curry-Howard Correspondence」。這個發現使得大家恍然大悟，「編寫程式」和「編寫證明」實際在概念上是完全統一的。而在這之後的 50 年，相關理論與技術發展使得證明不再停留在草稿紙上，而是可以用程式來表達。這個同構對映非常有趣：程式的型別對應於證明的定理；迴圈對應于歸納；……（這裡推薦一本書：『軟體基礎』（Software Foundations 中譯本）[6]）。在直覺主義框架中，證明就意味著構造演算法，構造演算法實際上就是在寫程式碼。(反過來也成立，嗯，碼農碼的不是程式碼，是數學證明，:P)
目前在電腦科學領域，許多理論的證明已經從紙上的草圖變成了程式碼的形式，比較流行的「證明程式語言」有 Coq，Isabelle，Agda 等等。採用程式設計的方式來構造證明，證明的正確性檢查可以機械地由程式完成，並且許多囉嗦重複性的勞動可以由程式來輔助完成。數學理論證明的大廈正在像計算機軟體一樣，逐步地構建過程中。1996 年 12 月 W. McCune 利用自動定理證明工具 EQP 證明了一個 長達 63 年曆史的數學猜想「Ronbins 猜想」，『紐約時報』隨後發表了一篇題為「Computer Math Proof Shows Reasoning Power」的文章[7]，再一次探討機器能否代替人類創造性思維的可能性。
利用機器的輔助確實能夠有效幫助數學家的思維達到更多的未知空間，但是「尋找證明」仍然是最有挑戰性的工作。「驗證證明」，則必須是一個簡單、機械、並且有限的工作。這是種天然的「不對稱性」。
八十年代：「證明」 == 「互動」
時間撥到1985年，喬布斯剛剛離開蘋果，而 S. Goldwasser 博士畢業後來到了 MIT，與 S. Micali，Rackoff 合寫了一篇能載入電腦科學史冊的經典：『互動式證明系統中的知識複雜性』[8]。
他們對「證明」一詞進行了重新的詮釋，並提出了互動式證明系統的概念：透過構造兩個圖靈機進行「互動」而不是「推理」，來證明一個命題在概率上是否成立。「證明」這個概念再一次被拓展。
互動證明的表現形式是兩個（或者多個圖靈機）的「對話指令碼」，或者稱為 Transcript。而這個對話過程，其中有一個顯式的「證明者」角色，還有一個顯式的「驗證者」。其中證明者向驗證者證明一個命題成立，同時還「不洩露其他任何知識」。這種就被稱為「零知識證明」。
再強調一遍，證明凝結了「知識」，但是證明過程確可以不洩露「知識」，同時這個證明驗證過程仍然保持了簡單、機械，並且有限性。這聽上去是不是有點「反直覺」？
互動式證明
上面例子就是一個「互動式證明」。假設Alice知道方程的解， f(w) = 0，那麼 Alice 如何讓 Bob 確信她知道 w 呢？Alice 在 「黑科技階段」 告訴了 Bob 一大堆的資訊。好了，關鍵問題是，Bob 能不能從 Alice 所說的一大堆資訊中猜出w 到底是幾，或者能分析出關於 w 的蛛絲馬跡呢？如果 Bob 有這個能力，Bob也許就沒必要掏錢了，因為他已經獲得了這個值錢的資訊。
請注意，如果 Alice 與 Bob 的對話是 「零知識」 的，那麼 Bob 除了知道 w 是 f(w)=0 的解之外，不能獲取其它任何關於 w 的資訊。這一點非常重要，這是保護 Alice 的利益。
現在回顧一下「零知識證明」這個詞，英文叫 「Zero-Knowledge Proof」 。這個詞包含三個關鍵部分：
· 零
· 知識
· 證明
各位可能已經有點感覺了，我們來嘗試著解讀一下：
· 零：Alice 洩露了關於 w 的「零」知識，也就是沒有洩露知識。
· 知識：這裡就是指的就是 w。
· 證明：就是Alice與Bob對話中的「黑科技部分」。
好了，證明也就是黑科技部分還沒講。看官們不要急，且聽我慢慢道來。
零知識證明有什麼用處？
一提零知識證明技術，很多人就想到了匿名 Coin，比如 Monero, 比如 ZCash。確實，這幾個 Coin 很好地普及了零知識證明，我本人也是透過 ZCash 才第一次聽說了零知識證明這個詞。但是在更深入地瞭解這個技術之後，深深感覺這個技術的威力遠不止這一點。
零知識證明技術可以解決資料的信任問題，計算的信任問題！
張三說他有100塊錢，李四說他北大畢業，王五說要和八菲特共進午餐。空口無憑，Show me the proof。
那麼「零知識證明」能解決資料的信任如何理解呢？在上一篇文章『zkPoD: 區塊鏈，零知識證明與形式化驗證，實現無中介、零信任的公平交易』[9]裡面，我提到了一個概念「模擬」：
零知識證明技術可以「模擬」出一個第三方，來保證某一個論斷是可信的
換句話說，當我們收到一個加了密的資料， 然後還有一個零知識證明。這個零知識證明是說 「關於資料的 X 斷言成立」，那麼這等價於有一個天使在我們耳邊悄聲說，「關於資料的X 斷言成立」！
對於這個 X 斷言，可以非常靈活，它可以是一個 NP複雜度的演算法。大白話講只要我們能寫一段程式（一個多項式時間的演算法）來判斷一個資料是否滿足 X 斷言，那麼這個斷言就可以用零知識證明的方式來表達。通俗點講，只要資料判定是客觀的，那麼就零知識證明就適用。
零知識證明的一些用處：
· 資料的隱私保護：在一個資料表格中，多多少少都有一些資訊不想被暴露，比如當年我的成績單，我只想向人證明，我的成績及格了，但是我不想讓別人知道我到底考了61分還是62分，這會很尷尬。我沒有心臟病，但是保險公司需要了解這一點，但是我不想讓保險公司知道我的隱私資訊。那我可以證明給保險公司看，我沒有心臟病，但是病歷的全部並不需要暴露。我是一家企業，我想向銀行貸款，我只想向銀行證明我具備健康的業務與還款能力，但是我不想讓銀行知道我們的一些商業秘密。
· 計算壓縮與區塊鏈擴容：在眾多的區塊鏈擴容技術中，Vitalik 採用 zkSNARK 技術能夠給現有的以太坊框架帶來幾十倍的效能提升。因為有了計算的證明，同樣一個計算就沒必要重複多次了，在傳統的區塊鏈架構中，同樣的計算被重複多次，比如簽名的校驗，交易合法性校驗，智慧合約的執行等等。這些計算過程都可以被零知識證明技術進行壓縮。
· 端到端的通訊加密：使用者之間可以互相發訊息，但是不用擔心伺服器拿到所有的訊息記錄，同時訊息也可以按照伺服器的要求，出示相應的零知識證明，比如訊息的來源、與傳送的目的地。
· 身份認證：使用者可以向網站證明，他擁有私鑰，或者知道某個只要使用者自己才知道的秘密答案，而網站並不需要知道，但是網站可以透過驗證這個零知識證明， 從而確認使用者的身份
· 去中心化儲存：伺服器可以向使用者證明他們的資料被妥善儲存，並且不洩露資料的任何內容。
· 信用記錄：信用記錄是另一個可以充分發揮零知識證明優勢的領域，使用者可以有選擇性的向另一方出示自己的信用記錄，一方面可以有選擇的出示滿足對方要求的記錄分數，同時證明信用記錄的真實性。
· 構造完全公平的線上數字化商品的交易協議[9]。
· 更多的例子，可以是任何形式的資料共享，資料處理與資料傳輸。
舉例：地圖三染色問題
下面講一個經典的問題，地圖的三染色問題。如何用三種顏色染色一個地圖，保證任意兩個相鄰的地區都是不同的顏色。我們把這個「地圖三染色問題」轉變成一個「連通圖的頂點三染色問題」。假設每個地區都有一個首府（節點），然後把相鄰的節點連線起來，這樣地圖染色問題可以變成一個連通圖的頂點染色問題。
下面我們設計一個互動協議：
「證明者」Alice
「驗證者」 Bob
Alice 手裡有一個地圖三染色的答案，請見下圖。這個圖總共有 6 個頂點，9 條邊。
現在 Alice 想證明給 Bob 她有答案，但是又不想讓 Bob 知道這個答案。Alice 要怎麼做呢？
Alice 先要對染過色的圖進行一些「變換」，把顏色做一次大挪移，例如把所有的綠色變成橙色，把所有的藍色變成綠色，把所有的綠色變成橙色。然後 Alice 得到了一個新的染色答案，這時候她把新的圖的每一個頂點都用紙片蓋上，然後出示給 Bob 看。
看下圖，這時候 Bob 要出手了（請見下圖），他要隨機挑選一條「邊」，注意是隨機，不讓 Alice 提前預測到的隨機數。
假設 Bob 挑選的是最下面的一條邊，然後告訴 Alice。
這時候 Alice 揭開這條邊兩端的紙片，讓 Bob 檢查，Bob 發現這兩個頂點的顏色是不同的，那麼 Bob 認為這次檢驗同構。這時候，Bob 只看到了圖的區域性，能被說服剩下的圖頂點的染色都沒問題嗎？你肯定覺得這遠遠不夠，也許恰好 Alice 蒙對了呢？其它沒暴露的頂點可能是胡亂染色的。
沒關係，Bob 可以要求 Alice 再來一遍，看下圖
Alice 再次把顏色做一次變換，把藍色改成紫色，改綠色改成棕色，把橙色改成灰色，然後把所有的頂點蓋上紙片。然後 Bob 再挑選一條邊，比如像上圖一樣，選擇的是一條豎著的邊，然後讓 Alice 揭開紙片看看，如果這時候 Bob 再次發現這條邊兩端的頂點顏色不同，那麼 Bob 這時候已經有點動搖了，可能 Alice 真的有這個染色答案。可是，兩次仍然不夠，Bob 還想再多來幾遍。
那麼經過反覆多次重複這三個步驟，可以讓 Alice 作弊並能成功騙過 Bob 的概率會以指數級的方式減小。假設經過 n 輪之後，Alice 作弊的概率為
這裡 |E| 是圖中所有邊的個數， 如果 n 足夠大，這個概率 Pr 會變得非常非常小，變得「微不足道」。
可是，Bob 每次看到的區域性染色情況都是 Alice 變換過後的結果，無論 Bob 看多少次，都不能拼出一個完整的三染色答案出來。實際上，Bob 在這個過程中，雖然獲得了很多「資訊」，但是卻沒有獲得真正的「知識」。
資訊 vs. 知識
· 資訊 「Information」
· 知識 「Knowledge」
在地圖三染色問題的互動證明中，當重複互動很多次之後，Bob 得到了大量的資訊，但是這好比 Alice 發給 Bob 一堆隨機數一樣，Bob 並沒有「知道」更多的東西。打個比方，如果 Alice 告訴 Bob 「1+1=2」，Bob 得到了這個資訊，可是 Bob 並沒有額外獲取更多的「知識」，因為這個事實人人皆知。
假如 Alice 告訴 Bob 2^2^41-1這個數是一個質數，很顯然這個是「知識」，因為要算出來這個數是不是一個質數，這需要耗費大量的算力。
假如 Alice 告訴 Bob，總共有兩個頂點用了綠顏色，那麼 Bob 就獲得了寶貴的「知識」，因為基於他剛剛獲取的這個資訊，Bob 可以用更短的時間用一臺圖靈機去求解三染色問題。假如 Alice 又透露給 Bob，最左邊的頂點顏色是用橙色，那麼很顯然，這個「資訊」對於 Bob 求解問題並沒有實質上的幫助。
我們可以嘗試定義一下，如果 Bob 在互動過程中獲得的「資訊」，可以幫助提升 Bob 直接破解 Alice 秘密的能力，那麼我們說 Bob 「獲得了知識」。由此可見，知識這個詞的定義與 Bob 的計算能力相關，如果資訊並不能增加 Bob 的計算能力，那麼資訊不能被稱為「知識」。比如在 Alice 與 Bob 互動過程中，Alice 每次都擲一個硬幣，然後告訴 Bob 結果，從資訊角度看，Bob 得到的資訊只是一個「事件」，然而 Bob 並沒有得到任何「知識」，因為 Bob 完全可以自己來擲硬幣。
下面引用『Foundations of Cryptography—— Basic Tools』一書[10]中的總結
「知識」是與「計算難度」相關，而「資訊」則不是
「知識」是與公共所知的東西有關，而「資訊」主要與部分公開的東西有關
注：曾有人問我，這裡的資訊與知識的定義是否與 Kolmogorov 複雜性有關。根據演算法資訊理論，一段字串的資訊量可以用產生字串的最小程式的長度來測量。這個問題我不是很懂，希望路過的專業人士留言。
可驗證計算與電路可滿足性問題
看了上面的地圖三染色問題，大家是不是沒有感覺，好像這只是一個學術問題，如何跟現實問題關聯起來？地圖三染色問題是一個 NP-Complete 問題，這是「計算理論」中的一個名詞。另外有一個叫做「電路可滿足問題」也是同樣是 NP-Complete 問題。NP-Complete 是一類問題，他的求解過程是多項式時間內難以完成的，即「求解困難」，但是驗證解的過程是多項式時間可以完成的，即「驗證簡單」。
那什麼是電路呢？下面是三個不同的「算術電路」：
可以看到一個電路由很多個門組成，其中有加法門，還有乘法門。每一個門有幾個輸入引腳，有幾個輸出引腳。每一個門做一次加法運算，或乘法運算。別看這麼簡單，我們平時跑的（沒有死迴圈）程式碼，都可以用算術電路來表示。
這意味著什麼呢？我們下面結合「零知識證明」與「電路可滿足性問題」來試著解決資料的隱私保護問題。
下面請思考一個場景：Bob 交給 Alice 一段程式碼 P，和一個輸入 x，讓 Alice 來執行一遍，然後把執行結果告訴 Bob。可能這個計算需要消耗資源，而 Bob 把計算過程外包給了 Alice。然後 Alice 執行了一遍，得到了結果 y。然後把 y 告訴 Bob。下面問題來了：
如何讓 Bob 在不執行程式碼的前提下，相信程式碼 P 執行的結果一定是 y 呢？
這裡是思考時間，大家可以想個五分鐘 ……
（五分鐘後……）
Alice 的一種做法是可以把整個計算過程用手機拍下來，這個影片裡面包含了計算機 CPU，還有記憶體，在整個執行過程中的每一電晶體的狀態。很顯然這麼做是不現實的。那麼有沒有更可行的方案呢？
答案是 Bob 把程式 P 轉換成一個完全等價的算術電路，然後把電路交給 Alice。Alice 只要計算這個電路就可以了，然後這個過程是可以用手機拍下來的，或者用紙記下來，如果電路規模沒有那麼大的話。Alice 只要把引數 6 輸入到電路，然後記錄下電路在運算過程中，所有與門相連的引腳線上的值。並且最後的電路輸出引腳的值等於 y，那麼 Bob 就能確信 Alice 確實進行了計算。Alice 需要把電路的所有門的輸入與輸出寫到一張紙上，交給 Bob，這張紙就是一個計算證明。
這樣 Bob 完全可以在不重複計算電路的情況下來驗證這張紙上的證明對不對，驗證過程很簡單：
Bob 依次檢查每一個門的輸入輸出能不能滿足一個加法等式或者一個乘法等式。
比如 1 號門是一個加法門，它的兩個輸入是 3，4，輸出是7，那麼很容易就知道這個門的計算是正確的。當 Bob 檢查完所有的門之後，就能確信：
Alice 確確實實進行了計算，沒有作弊。
這張紙上的內容就是「滿足」算術電路 P 的一個解「Solution」。
所謂的電路可滿足性就是指，存在滿足電路的一個解。如果這個解的輸出值等於一個確定值，那麼這個解就能「表示」電路的計算過程。
對於 Alice 而言，Bob 如果用這種方式驗證，她完全沒有作弊的空間。但是這種方法很顯然有個弊端：
· 弊端一：如果電路比較大，那麼證明就很大，Bob 檢查證明的工作量也很大。
· 弊端二：Bob 在驗證過程中，知道了所有的電路運算細節，包括輸入。
黑科技
我們再對剛才的 Alice 與 Bob 的場景做些修改。假如，Alice 自己還有一個秘密，比如說網銀密碼。而 Bob 想知道 Alice 的網銀密碼的長度是不是 20 位長。而 Alice 想了下，告訴他密碼長度應該問題不大。這時候 Bob 把一個計算字串長度的程式碼轉換成了電路 Q，並且發給 Alice。Alice 用電路 Q 算了一下自己的密碼，然後把電路所有門的引腳發給了 Bob，並帶上運算結果 20。
Wai……t，這是有問題的，Bob 拿到電路運算過程中的所有內部細節之後，不就知道密碼了嗎？是的，Alice 顯然不能這麼做。那麼 Alice 應該怎麼做？
答案是有很多種辦法，熱愛區塊鏈技術的讀者最耳熟的就是 zkSNARK[11]，還有zkSTARK[12]，子彈證明BulletProof[13]，以及一些比較小眾的技術，都可以幫 Alice 做到：
Alice 以一種零知識的方式，向 Bob 證明她計算過了電路，並且使用了她的秘密輸入。
換句話說，這些「零知識的電路可滿足性證明協議」為 Alice 提供了強大的武器來向 Bob 證明她的網銀密碼長度為 20，並且除此之外， Bob 再也得不到任何其它有用的資訊。除了網銀密碼，Alice 理論上可以向 Bob 證明任何她的隱私資料的某些特性，但是並不暴露任何別的資訊。
「零知識的電路可滿足性證明協議」提供了一種最直接的保護隱私/敏感資料的技術
最近幾年來，零知識證明構造技術發展日新月異，並且在區塊鏈技術領域得到了越來越多的應用。最新的零知識證明技術，有的技術可以讓 Bob 高速驗證證明（在移動裝置上幾毫秒驗證完成）；有的技術可以讓所有吃瓜群眾幫忙驗證（非互動式零知識證明）；有的技術支援非常小的證明大小（小到幾十個位元組）。後續文章我們會逐步展開介紹。
寫在最後
無論是精妙的數論定理，地圖三染色問題，還是電路可滿足性問題。證明存在的意義是什麼？所有的證明都體現了「證明」與「驗證」的「不對稱性」。證明可能是一個非常耗費算力，或者腦力的活動，無論是耗時幾百年的「費馬大定理」，還是比特幣中的 POW 證明，這些證明都凝結了在尋找證明過程中所消耗的能量，證明過程可能是超乎尋常的複雜，偶爾需要天才橫空出世。而驗證過程一定（或者應該）是一個非常簡單的，機械的，在（多項式）有效時間內且能終止的活動。某種意義上，這個不對稱性真正體現了證明的意義，展示了零知識證明的價值。
粗略看，「證明」是「邏輯」的產物，但「邏輯」與「計算」卻又有著密不可分的聯絡，大家可能模模糊糊感覺到一些關於「證明」與「計算」之間的關聯，它們貫穿始終：如機械推理、證明表達、互動計算 。這是一個有趣但更巨集大的哲學問題。
參考文獻
[1] 西蒙, 辛格, 薛密. 費馬大定理: 一個困惑了世間智者 358 年的謎[M]. 上海譯文出版社, 1998.
[2] Alec Wilkinson. The Pursuit of Beauty: Yitang Zhang solves a pure-math mystery. The New Yorker. Feb. 2015.
[3] 馬丁, 戴維斯, 張卜天. 邏輯的引擎[M]. 湖南科學技術出版社, 2012.
[4] Raymond Smullyan. Gödel's Incompleteness Theorems, Oxford Univ.Press. 1991.
[5] Turing, Alan. "On computable numbers, with an application to the Entscheidungsproblem." Proceedings of the London mathematical society 2.1 (1937): 230-265.
[6] Pierce, Benjamin C., et al. "Software foundations." 中文譯文: <https://github.com/Coq-zh/SF-zh
[7] Kolata, Gina. "Computer math proof shows reasoning power." Math Horizons 4.3 (1997): 22-25.
[8] Goldwasser, Shafi, Silvio Micali, and Charles Rackoff. "The knowledge complexity of interactive proof systems." SIAM Journal on computing 18.1 (1989): 186-208.
[9] zkPoD: 區塊鏈，零知識證明與形式化驗證，實現無中介、零信任的公平交易. 安比實驗室. 2019.
[10] Oded, Goldreich. "Foundations of cryptography basic tools." (2001).
[11] Gennaro, Rosario, et al. "Quadratic span programs and succinct NIZKs without PCPs." Annual International Conference on the Theory and Applications of Cryptographic Techniques. Springer Berlin, Heidelberg, 2013.
[12] Ben-Sasson, Eli, et al. "Scalable, transparent, and post-quantum secure computational integrity." IACR Cryptology ePrint Archive 2018 (2018): 46.
[13] Bünz, Benedikt, et al. "Bulletproofs: Short proofs for confidential transactions and more." 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 2018.
