1957 年 、 多く の 論理 学者 と 計算 機 科学 者 が 一堂 に 会し た Cornell Summer が 自動 推論 または 自動 定理 証明 の 起源 と さ れる こと が ある 。

Logic Theorist ( LT ) は 1956 年 、 アレン ・ ニューウェル 、 クリフ・ショー 、 ハーバート・サイモン が 開発 し た 人間 の 行う 推論 を 真似 て 定理 を 証明 する プログラム で あり 、 『 プリンキピア・マテマティカ 』 の 第 2 章 に ある 52 の 定理 の うち 38 を 証明 し て みせ た 。

自動 推論 の 最大 の 応用 は 自動 定理 証明 機 の 構築 で ある 。

時に は そういった 証明 機 が 定理 の 新た な 証明 方法 を もたらす こと も あり 、 Logic Theorist が よい 例 で ある 。

また 、 CADE という 学会 で 定期 的 に 自動 定理 証明 機 の 競技 会 が 開催 さ れ て おり 、 競技 会 で 使用 する 問題 は TPTP ライブラリ から 選ば れ て いる 。

これ は 1930 年代 の アラン ・ チューリング や ライス の 研究 で 判明 し た （ チューリングマシン の 停止 問題 および ライス の 定理 ） 。

特に （ 最初 は 認識 さ れ なかっ た が ） ボルツマン の H 定理 （ 1872 年 ： エントロピー の 不可逆 的 増大 を 説明 する ） で この 仮定 が 重要 な 基礎 と なっ て いる 。

これ を 用い て 分布 関数 に関する ボルツマン 方程式 を 計算 する こと で 、 H 定理 が 証明 さ れる 。

1940 年代 における 代数 的 位相 幾何 学 の 発展 により 、 空間 の 直積 と ホモロジー 群 の テンソル 積 と の 対応 （{ 仮 リンク | キュネット の 定理 | en | Künneth theorem }） など の 理解 の ため に も テンソル 積 を 純 代数 的 に 定式 化 し 取り扱う 必然 性 が 生まれ て い た 。

一方 で 、 主 に 他 地域 の 経済 学者 から 、 MM 定理 （ 自己 資金 で 事業 を おこなう より も 、 借入 を し た ほう が 金利 分 が 経費 処理 できる ので 、 税制 面 で 有利 で ある こと ） を 出す まで も なく 、 借金 を し て 事業 拡大 する こと を 週刊 誌 等 で たびたび 提案 さ れる が 、 経営 状態 の よい 会社 は 「 貸し たい 側 の 理屈 」 として 初め から 相手 に し て い ない 。

これ を 体積 V で 積分 する と 、 発散 定理 を 用い て と なる 。

これ を 対称 式 の （ 第 一 ） 基本 定理 と いう 。

この 基本 対称 式 に関する 多項式 g を 具体 的 に 見いだす アルゴリズム は 複数 知ら れ て おり 、 それら は 、 基本 定理 の 証明 を 与え て も いる 。

1762 年 に ウェア リング は 、 対称 式 に 現れる 単項式 の 指数 の 組 に 、 辞書 式 順序 を 入れ て 、 単項式 の 次数 を 下げ て いく 方法 で 、 対称 式 の 基本 定理 の 証明 を 行っ た 。

n = 1 の 時 は 対称 式 の 基本 定理 は 明らか に 成り立つ ので 、 数学 的 帰納 法 により 、 n 変数 の 対称 式 について 基本 定理 が 成り立つ 。

後に ジョン ・ ナッシュ は これ を 発展 さ せ た ナッシュ の リーマン 多様 体 埋め込み 定理 を 証明 し た 。

オイラー 予想 （ オイラー よそう ） と は 、 スイス の 数学 者 レオンハルト・オイラー が 提唱 し た 、 フェルマー の 最終 定理 を 発展 さ せ た 数学 的 予想 で ある 。

ハーディ と ライト の 『 数 論 入門 』 に は 、 コープ ランド - エルデシュ 定数 が 無理 数 で ある こと の 直接 の 証明 として 、 算術 級数 定理 を 用い た もの と 、 ベルト ラン の 仮説 を 用い た もの が 紹介 さ れ て いる 。

一連 の 整式 の 最後 の 整式 が 定理 と 認識 さ れる 。

ある 形式 体系 が 与え られ た とき 、 定理 群 を 定義 でき 、 それら を その 形式 体系 内 で 証明 できる 。