フーリエ の 定理 に よれ ば 、 任意 の 周期 関数 は 正弦 波 の 級数 で 表せる （ フーリエ 級数 ） 。

特異 値 分解 は 、 行列 に対する スペクトル 分解 定理 の 一般 化 と も 考え られ 、 正方 行列 に 限ら ず 任意 の 形 の 行列 を 分解 できる 。

多項式 { math | P ( x ) {{=} x { sup | 2 } − 2 }} に対して 有理 根 定理 を 適用 する 。

有理 根 定理 に よれ ば 、 { mvar | p , q } を 互いに 素 な 整数 として 、 多項式 の 有理 根 が { math | x {{=} p & thinsp ;/& thinsp ; q }} と 表せる とき 、 { mvar | p } は 定数 項 の 約数 で あり 、 { mvar | q } は 最高 次 の 係数 の 約数 で ある 。

アルゴリズム の 停止 性 は 無限 の 猿 定理 により 保証 さ れる 。

外角 定理 （ がい かく て い り ） と は 、 三角形 において 2 つ の 内角 の 和 は 隣り 合わ ない 1 つ の 外角 と 等しい 事 を 示す 定理 。

フライ 曲線 は フェルマー の 最終 定理 を 解決 する 有力 な 手がかり と なっ た 。

1996 年 に フェルマー の 最終 定理 に関する 研究 で ガウス・メダル を 受賞 し た 。

自動 定理 証明 （ automated theorem proving 、 ATP ） と は 、 自動 推論 ( AR ) の 中 で も 最も 成功 し て いる 分野 で あり 、 コンピュータ プログラム によって 数学 的 定理 に対する 証明 を 発見 する こと 。

ベース と なる 論理 によって 、 定理 の 妥当 性 を 決定 する 問題 は 簡単 な もの から 不可能 な もの まで 様々 で ある 。

1920 年 、 トアルフ・スコーレム は { 仮 リンク | レオポールト・レーヴェンハイム | en | Leopold Löwenheim } の 成果 を 単純 化 し た レーヴェンハイム - スコーレム の 定理 を もたらし 、 1930 年 に は エルブラン 領域 と エルブラン 解釈 により 、 一 階 の 論理 式 の 充足 （ 不 ） 可能 性 （ および 定理 の 妥当 性 ） を 命題 論理 の 充足 可能 性 問題 に 還元 できる こと が 示さ れ た 。

ヒューリスティック による 誘導 を 使っ て おり 、 『 プリンキピア・マテマティカ 』 の 52 の 定理 の うち 38 の 証明 に 成功 し た 。

Logic Theorist の ヒューリスティック と は 人間 の 数学 者 の エミュレート を 試みる こと で あり 、 妥当 な 定理 すべて について 証明 できる こと を 保証 でき なかっ た 。

命題 論理 の 多く の 問題 で は 、 定理 は 決定 可能 だ が co - NP 完全 問題 で あり 、 汎用 的 な 証明 に は 指数 時間 アルゴリズム しか ない と 考え られ て いる 。

（ 適切 な ） 公理 を 持た ない 一 階 述語 論理 で は 、 ゲーデル の 完全 性 定理 によって 定理 と 論理 的 に 妥当 な 整 論理 式 に 対応 し て おり 、 定理 の 識別 は 再帰 的 に 枚挙 可能 で ある 。

すなわち 、 無限 の リソース を 前提 と すれ ば 、 任意 の 有効 な 定理 を 証明 できる 。

無効 な 文 、 すなわち 与え られ た 定理 から 導け ない 式 は 認識 可能 と は 限ら ない 。

さらに ゲーデル の 不完全性 定理 に よれ ば 、 一 階 述語 論理 の 一貫 し た 理論 は その 体系 内 で 証明 でき ない 真 の 論理 式 を 含む こと が ある 。

その よう な 場合 、 一 階 述語 論理 の 定理 証明 機 は 証明 探索 の 完了 に 失敗 する 可能 性 が ある 。

この よう な 理論 上 の 制限 は ある が 、 実用 的 な 定理 証明 機 は 様々 な 難しい 問題 の 証明 を する こと が できる 。