數學理論的無矛盾性有了這種有限的、可構造性的論證之后，任何人都可以放心了。希爾伯特計劃提出后，幾組數學家分別為實現它而努力：一組是希爾伯特及貝耐斯，以及阿克曼關于把數學理論形式化的研究，一組是馮·諾依曼關于算術無矛盾性的初步研究及哥德爾的不完全性定理以及甘岑的最后解決；還有一組是厄布朗及甘岑關于證明的標準形式等的研究。

厄布朗是法國天才的青年數學家，1931年8月在登阿爾卑斯山時遇難，年僅23歲。他對代數數論尤其是數理邏輯進行過重要的研究工作，1929年他在博士論文《證明論研究》中提出他的基本定理。從某種意義上來講，這個定理是想把謂詞演算歸結為命題演算。由于前一理論是不可判定的，而后一理論是可判定的，因此這種歸結不可能是完全的。

但是，由于厄布朗局限于希爾伯特有限主義立場，他應用的證明方法比較繞彎子。而且在1963年發現，他的證明中有漏洞，他的錯誤很快就得到了彌補。厄布朗定理可以便我們在證明中擺脫三段論法。他的許多結果，后來也為甘岑獨立地得出。

甘岑的自然演繹系統是把數學中的證明加以形式化的結果。他由此得出所謂“主定理”，即任何純粹邏輯的證明，都可以表示成為某種正規形式，雖然正規形式不一定是唯一的。為了證明這個主定理，他又引進了所謂的式列演算。

在普通的數學證明中，最常用則是三段論法，即如果A→B，且若A成立，則B成立。其實這就是甘岑推論圖中的“斷”。但是甘岑的主定理就是從任何證明圖中可以消除掉所有的“斷”。也就是：如果在一個證明中用到三段論法，那么定理表明，它也可以化成為不用三段論法的證明，也得到同樣的結論。

這個定理乍一看來似乎不可理解，其實正如甘岑所說，一個證明圖中有三段論法實際上是“繞了彎子”，而不用三段論法是走直路。這種沒有三段論法的證明圖稱為“正規形式”，利用這沒有三段論法的證明圖稱為“正規形式”。利用這個主定理很容易得出許多重要結果，其中之一就是極為簡單地證明“一階謂詞演算是無矛盾的”，而且能夠推出許多無矛盾性的結果。后來還可以用來證明哥德爾的完全性及不完全性定理，當然，最重要的事還是要證明算術的無矛盾性。

希爾伯特引進證明論的目標是證明整個數學的無矛盾性，其中最重要的是集合論的無矛盾性(至少ZF系統無矛盾)、數學分析的無矛盾性，最基本的當然是算術的無矛盾性。哥德爾的不完全性定理說明，用有限的辦法這個目標是達不到的。由于哥德爾不完全定理的沖擊，希爾伯特計劃需要修改。

有限主義行不通就要用非有限的超窮步驟。1935年，甘岑用超窮歸納法證明自然數算術形式系統的無矛盾性。其后幾年，他和其他人又給出了其他的證明。這種放寬了的希爾伯特計劃在第二次世界大戰之后發展成為證明論的分支，這些證明也推廣到分支類型論及其他理論。

甘岑在第二次大戰行將結束時去世，他的結果代表當時證明論的最高成就，希爾伯特和貝納斯的《數學基礎》第二卷中總結了他的工作，但是證明論遠遠未能完成它的最初目標。戰后隨著模型論和遞歸論乃至六十年代以來公理集合論的發展，證明論一直進展不大。

五十年代中，日本數學家竹內外史等人開始對于實數理論(或數學分析)的無矛盾性進行探索。因為實數一開始就同有理數的無窮集和有關，描述它的語言用一階謂詞演算就不夠了，所以第一步就要先把甘岑的工作推廣到高階謂詞演算中去。

1967年，日本年輕數學家高橋元男用非構造的方法證明，單純類型論中也可以消去三段論法。由此可以推出數學分析子系統的無矛盾性。但是，由于證明不是構造的，數學分析的無矛盾性至今仍然有待解決。

厄布朗及甘岑的結果雖然不可能完成希爾伯特計劃的最初目標，但是由于其有限性、可構造性的特點，現在已廣泛地應用于機械化證明，成為這門學科的理論基礎。

證明論的方法對于數理邏輯本身有很大的推動，特別是得出新的不可判定命題。最近，英國年輕數學家巴黎斯等人有了一項驚人的發現。他們發現了一個在皮亞諾算術中既不能證明也不能否證的純粹組合問題，這不僅給哥德爾不完全性定理一個具體的實例，而且使人懷疑要解決許多至今尚未解決的數論難題可能都是白費力氣。這無疑開辟了證明論一個完全新的方向。