システム管理者
ヒルベルトの計画（綱領）
ヒルベルトは，1921年に「ヒルベルトの計画（綱領）」を発表します．すべての数学を公理形式で記述したいのですが，その基礎になる公理の独立性，一貫性が保証されなければなりません．ヒルベルトは，1900年に行われた講演「23の数学的問題」の2番目でもこの問題を取り上げています．
20世紀初頭は，数学者はますます複雑な問題への挑戦を進めるが，その一方で，数学への基本的な疑問も起こりました．数学とは何か？その基本法則は何か？
ダーフィト・ヒルベルトには，数学の本質に取り組むための大胆なアイデアがありました．彼は数学を骨抜きにし，単なるゲームとして扱おうと考えました．チェスがポーンやキャッスルといった駒を使ってプレイされるように，数学ゲームも基本的な構成要素は記号： 0，1，+，×，=，などで，これらを組み合わせてすべての数学が出来ています．
数学を記号のゲームに落とし込み，記号の「意味」を忘れることで，数学とは何か，その基本的なルールが現れて来ると考えました．
数学の原理「ルールの基本セット」が見つかれば，これを根拠にすべての数学的記述の証明ができるし，数に関するどのような数学的記述も真か偽かをこれで決定できます．ヒルベルトは，算術の構造の根底にある論理を利用して，究極の数学理論を見つけたいと考えました．
残念ながら，ヒルベルトの計画（綱領）が実現することはなかった．
クルト・ゲーデルもヒルベルトの計画に触発された一人で，不完全性定理の研究を行い，数学が成り立つ完全なルール・セットは誰も作れないことを証明しました．
ゲーデルの証明によれば，公理系に矛盾がなく完全であることの証明は，公理系の枠組みでできない．完全性（あるいは不完全性）を証明したり反証したりするには，公理の追加（システムの強化）が必要である．
その後，アラン・チューリングのアルゴリズムに関する研究は，任意の数学的記述の真偽を評価できる手続き（アルゴリズム）は存在し得ないことを示しました．
しかし，数値システムをゲームとして扱うという彼の「形式主義的」アプローチは，数理論理学への新たな関心を呼び起こしました．
すべての数学的問題を解決することはできないが，問題のいくつかの特殊なサブクラスは，この方法で解決することができます．今日の数学者たちは，ヒルベルトの計画から肯定的な結果を救出し続けています．
ゲーデル
算術は，0，1，2，3...という整数の体系と，それらを組み合わせる方法：加算，減算，乗算，除算で成り立ちます．19世紀後半になると，数学の基本法則を見つけることに焦点が当てられ，数学者たちが求めていたのは，算術の基本法則（ルール）のリストです．すべての数学定理は，そのルールセットから論理的に演繹できるはずです．バートランド・ラッセルとアルフレッド・ノース・ホワイトヘッドによる3巻の著作『プリンキピア・マテマティカ』(1996年)を筆頭に，いくつかのルールブック候補が登場しました．
これは，基本的仮定のリストから数学の全体を構築しようとするものであったのです．しかし，1931年，クルト・ゲーデルは，そのような完全なルールブックを作ることは不可能であるという定理を証明してしまいました．
整数に関する記述の中には，真であるにもかかわらず推論できないものが必ずある．
もちろん，ルールブックを拡張してこの記述を新しい法則として組み込むことはできるが，それでも理論には他のギャップが残ることになる．ゲーデルの定理は，それらをすべて埋めることは決して望めないことを保証しています．
その後，算術の論理体系の階層が構築され，それぞれの体系が下の体系（サブクラス）のギャップの多くを埋めていることが知られます．
「証明理論」のテーマは，これらの異なる体系の論理的な強さを比較しています．
一方，「逆数学」では，古典的な数学の結果が成立する基盤条件の理解を狙い， 与えられた定理の証明にどのような公理があるのかを正確に調べています．