在20世紀初數學奠基問題的論戰中，由D.希爾伯特提出的旨在保衛古典數學、避免悖論以解決數學奠基問題的一種方案。又稱證明論計畫。
20世紀初，悖論尤其是羅素悖論的出現動搖瞭傳統的數學概念、數學命題和數學方法的可信性標準，從而引起所謂第三次數學基礎危機。直覺主義者從他們的直覺主義數學觀出發，否定實無窮，堅持“存在”即被構造，排斥康托爾集合論和傳統邏邏輯的排中律，否認古典數學中的大量的非構造性定義和純存在性證明。希爾伯特認為：這是不可取的，是錯誤的途徑。他希望保衛古典數學。在希爾伯特看來，每一門數學都可以看成是基於它的公理的一個演繹系統，它們是根本不會產生邏輯矛盾的，亦即是協調的。為此，希爾伯特提出瞭著名的證明論計劃，其基本內容為：
①將所要討論的古典數學理論T(有內容的)(如數論)公理化，把所得的公理化理論和所用的邏輯徹底地形式化，使得有內容的古典數學理論T(如數論)能表示成一些形式符號和形式符號公式(它們是沒有內容的)組成的系統，記為TF。它使得表達現實命題和理論命題在方法上協調起來成為可能，通過對形式理論TF的協調性的研究來建立原來的古典數學理論T的可靠性。
②由於研究形式理論TF時需要用到邏輯和數論，故希爾伯特建議采用有窮方法來建立一個邏輯系統和初等數論，以便與經典邏輯和普通數論相區別，從而避免循環論證。這樣建立起來的邏輯和數論，希爾伯特稱之為元數學(見證明論)。
③用元數學來證明在形式理論TF中，不會有某個論斷A與其否定可以同時推出，也就是證明形式理論TF的協調性。如果形式理論TF的協調性能夠元數學地證明，則TF所摹寫的古典數學理論及其理想命題都可以保留。
希爾伯特計劃約在1922年問世，它的問世吸引瞭許多數學傢為促其實現而努力。一些較為簡單的對象理論，諸如命題演算、一階謂詞演算（見謂詞演算），隻含加法的算術等的協調性已被先後證得。但是1931年K.哥德爾發表的著名的不完全性定理給希爾伯特的證明論計劃以沉重打擊。希爾伯特本人雖因此而感到震驚，但並不認為自己的計劃已被否定，而認為隻需將有窮方法加以擴充，再增加超限歸納法作為證明論的工具，原計劃還是可行的。1936年，G.根岑用超限歸納法證明瞭純數論的協調性，但這已不是希爾伯特原來的計劃。
總之，希爾伯特的計劃雖然沒有實現，但它對現代數學的發展有很大的促進作用。在它的直接影響、啟迪和促進下，推動瞭大量的新思想、新見解和新知識的出現，而元數學作為數理邏輯的重要分支正生氣勃勃地發展著。
推薦書目
王浩. 數理邏輯通俗講話. 北京: 科學出版社, 1981.
王憲鈞.數理邏輯引論.北京: 北京大學出版社, 1982.
克林 S C. 元數學導論. 莫紹揆, 譯. 北京: 科學出版社, 1984.