又稱證明論計畫，是在20世紀初數學奠基問題的論戰中，由D.希爾伯特提出的旨在保衛古典數學、避免悖論以解決數學奠基問題的一種方案。
20世紀初，悖論尤其是羅素悖論的出現，引起瞭當時數學界和邏輯界的極大震動。它直接衝擊瞭以嚴謹著稱的數學和邏輯學科，動搖瞭傳統的數學概念、數學命題和數學方法的可信性標準，也就是說悖論的出現關係到整個數學的奠基問題，從而引起所謂第三次數學基礎危機。
以L.E.JJ.佈勞威爾為代表的直覺主義者（見數學基礎）從他們的直覺主義數學觀出發，否定實無窮，堅持‘存在’即被構造，排斥康托爾集合論和傳統邏輯的排中律，否認古典數學中的大量的非構造性定義和純存在性證明，從而擯棄瞭大部分古典數學成果。希爾伯特認為：這是不可取的，是“錯誤的途徑”。他認為古典數學(包括康托爾集合論)是“我們最有價值的寶藏”，而傳統邏輯中的“排中律”是普遍有效的，希望保存這種古典數學的“有成效的概念結構和推理方法”。也就是說，希爾伯特是希望保衛古典數學的。同時，希爾伯特也認為：“絕對無窮概念的命題確實是超越人們直觀性證據之外”的東西，“是通過人們的心智過程被插入或外推出來的概念”。但是，數學的各個分支都涉及無窮集合，例如數學分析它在一定的意義上就是一首“無窮的交響樂”。可見，無窮在思維過程中是不可缺少的，應有其適當的位置。由於無窮不能在經驗中直接驗證，故希爾伯特稱之為理想元素，並將古典數學中以實無窮為前提的命題稱做理想命題，反之將有直觀意義的命題稱做現實命題。希爾伯特認為：理想元素方法在數學中是常用的，行之有效的方法。如在幾何中引進瞭無窮遠點以後，不僅有“兩不同點可決定惟一直線”而且還可以有“兩不同直線可以決定惟一的一個點”。在代數中引進瞭虛數i以後，就可以簡化方程式根的定理，因此盡管理想元素可能沒有意義，但是由它可以推出有意義的元素和定理來，並可以簡化理論結構。希爾伯特從而將古典數學分成涉及實無窮的“理想數學”和以“有窮主義”為特征的現實數學（即構造性數學）。希爾伯特與他的弟子P.貝爾奈斯曾對“有窮主義”一詞作如下解釋：“我們常用&lsquo；有窮'一詞放在別的表達式之前，表示有關的考慮，斷言或定義均限於基本上可以想象的對象以及基本上可以完成的過程，從而可以在具體處理的范圍內加以完成。”簡言之，希爾伯特的有窮方法是指不涉及實無窮的、直觀上明顯可靠的、能在有窮步驟內根據確定的機械的辦法實施的，並可終結。希爾伯特認為：產生悖論的原因不在於“實無窮”，而在於對“實無窮”的錯誤認識；問題不在於使用理想元素，而在於說明使用理想元素不會帶來矛盾。實際上，希爾伯特所創立的形式公理法當時已被廣泛沿用，E.F.F.策梅洛據以建立的第一個集合論公理系統即公理集合論已能排斥已知集論悖論，同時又能發展集論中原有合理的有效內容，所以問題確實在於進一步說明不會產生新的悖論。
在希爾伯特看來，每一門數學都可以看成基於它的公理的一個演繹系統，它們是根本不會產生邏輯矛盾的，亦即是協調的。數學的可靠性就在於它的協調性（即無矛盾性）。協調性問題在非歐幾裡得幾何學創立時曾經討論過，當時為瞭證得非歐幾何的協調性是把它化歸到歐氏幾何的協調性，即如果歐氏幾何無矛盾則非歐幾何亦無矛盾。這是一種相對的證明方法，若要證明整個數學無矛盾，就不能再用這種化歸的方法，而是要求給出“絕對的”證明。為此，希爾伯特提出瞭著名的證明論計劃，其基本內容為：
① 將所要討論的古典數學理論T（有內容的）（如數論）公理化，把所得的公理化理論和所用的邏輯徹底地形式化，使得有內容的古典數學理論T（如數論）能表成一些形式符號和形式符號公式(它們是沒有內容的)組成的系統，記為TF，TF形式地摹寫瞭T中的現實命題和理想命題以及其間的邏輯關系。這種形式符號系統TF稱為T的形式理論（如形式數論），TF是作為一種獨立結構而存在的，它使得表達現實命題和理論命題在方法上協調起來成為可能，並且使得所用的邏輯也可以得到一個“確切、科學的處理”。通過對形式理論TF的協調性的研究來建立原來的古典數學理論T的可靠性。
② 由於研究形式理論TF時需要用到邏輯和數論，故希爾伯特建議采用有窮方法來建立一個邏輯系統和初等數論，以便與經典邏輯和普通數論相區別，從而避免循環論證。這樣建立起來的邏輯和數論，希爾伯特稱之為元數學（見證明論）。將用Tm來討論TF的協調性，Tm中的符號和公式是有內容的。對TF的討論采用構造的方法，不得涉及實無窮。這一點希爾伯特與佈勞威爾是一致的。
③ 用元數學Tm來證明在形式理論TF中，不會有某個論斷A與其否定¬A同時可以推出，也就是證明形式理論TF的協調性。如能證得TF的協調性就可以保證所代表的古典數學理論T不會產生矛盾。換言之，如果形式理論TF的協調性能夠元數學地證明，則TF所摹寫的古典數學理論及其理想命題都可以保留。
這就是希爾伯特證明論計劃的主要步驟。
希爾伯特在計劃中區分瞭三種數學理論。第一種是古典的（即普通的）數學理論T，T是直觀的、非形式的，T中的符號和公式都是有內容的。第二種是形式數學理論TF，TF是一個形式符號系統，它是第一種數學理論的形式化，將通過證明TF的協調性來建立古典數學的可信性，TF通稱為對象理論，對象理論TF中的符號和公式都是沒有內容的、純形式的，但TF的系統特征(如協調性)即可用符號排列的組合來表述。第三種數學理論Tm是用來描述和研究第二種數學理論的，希爾伯特稱Tm為元數學或證明論，在元數學中，人們應按前述的“有窮主義”辦事。也就是說，希爾伯特認為可信性隻存在於有限之中，而理想元素隻是理性規定而已。這一點他與直覺主義是相通的，並將這一觀點貫徹在元數學中。其目的在於證明對象理論的協調性。從而給出TF所代表的古典數學理論T的無矛盾性的絕對證明。
希爾伯特在他的計劃中強調瞭兩個原則：其一為徹底地形式化；其二為有窮主義。無前者則一門古典數學理論及其所用的邏輯將無從得到精確表達，因而不能成為確定的研究對象；無後者則難以保證所用工具不超過系統TF內所有的工具，無法避免循環論證。
希爾伯特在他的計劃中突出瞭一個目的：要通過元數學Tm來證明對象理論TF的協調性，以說明TF所代表的古典數學理論T是不會產生矛盾的，從而保衛古典數學成果。
希爾伯特計劃約在1922年問世，曾經引起相當普遍的重視，吸引瞭許多數學傢（包括象哥德爾這樣的大數學傢）為促其實現而努力。一些較為簡單的對象理論，諸如命題演算，一階謂詞演算，隻含加法的算術等的協調性已被先後證得，這些工作促進瞭數理邏輯的發展也增強瞭對計劃的信心。但是1931年K.哥德爾發表瞭著名的不完備性定理（見哥德爾不完備性定理）；這給希爾伯特的證明論計劃以沉重打擊。希爾伯特本人雖因此而感到震驚，但並不認為自己的計劃已被否定，而認為隻需將有窮方法加以擴充，再增加超限歸納法作為證明論的工具，原計劃還是可行的。1936年G.根岑用超限歸納法證明瞭純數論的協調性，但這已不是希爾伯特原來的計劃。希爾伯特的計劃雖然未能實現，但它對現代數學的發展有很大貢獻。
① 它創立瞭元數學（證明論），在使用瞭公理化方法和形式化方法以後，它第一次使一門數學理論整體地作為一個確定的、可用數學方法來研究的研究對象；它使得用來說明古典數學理論無矛盾的、形式理論的協調性能予精確表示；它使得現實命題和理想命題表達方法的一致成為可能。這些都是超越前人、令人欽服的新思想。同時，事實證明，這樣把一種理論整體地作為研究對象用另一種理論加以研究是很有成效的。常常能夠得到許多新的見解。這對現代數學和計算機科學的發展都是很有意義的。
② 希爾伯特在計劃中提出瞭一個可信性標準：數學的可信性在於它的協調性。與其同時代的佈勞威爾或羅素的主張相比較，這更易為大多數的數學傢所樂於接受。所以，當希爾伯特計劃問世後，曾經吸引相當多的追隨者為之奮鬥。特別是哥德爾原來也是想實現希爾伯特計劃的，但在實踐中發現這是不可行的，而後他才建立瞭著名的不完備性定理。這就是說，哥德爾原來也是贊同希爾伯特的可信性標準的。不完備性定理這一劃時代成果是在實踐這一標準的過程中發現的。
③ 希爾伯特在計劃中所倡導的有窮主義的構造方法即是一種以有窮主義為特征的構造性數學研究。這也是現代構造性數學的一支。這一研究曾為希爾伯特的弟子貝爾奈斯和克萊塞等的工作所繼續發展。
④ 使用元數學方法，對於數理邏輯本身亦有很大推動。英國的帕裡斯等由此得出瞭新的不可判定問題。他們發現瞭一個在皮亞諾算術中既不能證明也不能否證的純粹的組合問題，它不僅給哥德爾不完備性定理一個具體實例，而且使人懷疑要解決許多尚未解決的數論難題，可能是白費力氣，應另作他圖。
總之，希爾伯特的計劃雖然沒有實現，但它對現代數學的發展有很大的促進作用。希爾伯特企圖把有窮主義觀點下的構造性與涉及實無窮的理想元素在應用上的有效性統一起來，這一願望雖然不能實現，但在它的直接影響、啟迪和促進下，推動瞭大量的新思想、新見解和新知識的出現，並且創建瞭象元數學這樣重要的、有深遠影響的新分支，這對現代數學的發展很有貢獻。元數學（證明論）作為數理邏輯的重要分支正生氣勃勃地發展著。