現時点でたくさんの機械数学が存在します。
Formalizing 100 Theorems には有名な定理と共に、どの機械数学で証明済みかが載っています。

主な機械数学

システム名派閥（ベース理論）開発開始年主な創始者
Lean型理論派 (依存型理論)2013年Leonardo de Moura
Coq型理論派 (構造型理論)1989年Gérard Huet
Thierry Coquand
Isabelle型理論派 (高階論理)1986年Lawrence Paulson
HOL Light型理論派 (高階論理)1993年John Harrison
Mizar集合論派 (TG集合論)1973年Andrzej Trybulec
Metamath集合論派 (ZFC集合論)1992年Norman Megill
ACL2独自のLisp論理 (一階論理)1990年Matt Kaufmann
J Strother Moore

主流派

現在の主流は「型理論」です。
「計算機にとって扱いやすい証明体系」と「巨大な形式化ライブラリ」が作られています。
中でもLeanは2020年代以降、自動証明AI（DeepSeek-Proverなど）の格好の実験場となり、現在の中心的な存在になっています。

現代のコンピュータ科学において、多くの開発者が「型理論」に流れてしまうのには、彼らなりの（数学的というよりは）「計算機的な都合」があります。

  • プログラマの直感: コンピュータのプログラムは「型（Int、Stringなど）」でバグを防ぎます。そのため、計算機科学出身の形式化研究者は「数学も型で管理すれば、不条理な証明や \(1 \in \pi\) のような無意味な式を未然に防げる」と考えがちです。
  • 型チェックの軽さ: 型理論は、「型が一致しているか」を調べるだけで論理の正しさを高速にチェックできる（Curry＝Howard同型対応）ため、コンピュータにとって処理が書きやすかったのです。

しかし、その代償として、数学者が黒板に書くような「自由で柔軟な数学の視点の切り替え」を犠牲にしているのが、今の主流派の限界です。

その他の派と私たちの立場

「集合論派」は数学本来のクラシック・王道の設計です。
私たちはそれを現代の(特にAI)技術でアップデートしようとしています。
一階論理と集合論を土台に、人間に読みやすい数学記述と機械による自動証明を両立させる道を探っています。

Metamathとは次のものを共有しています。
・「純粋な一階論理と集合論だけで数学を構築する」という始まりの思想
・「クラスを消去可能な略記として一階論理に落とす」という設計
ライブラリはHilbert流の公理系からスタートし、証明器の核を極限まで小さくしていますが、私たちは「一階言語は既知とされる」というスタンスをとっています。

Mizarは集合論形式化の最長老であり、次のものを共有しています。
・素朴な「数学論文をそのままコンピュータに読ませたい」という情熱
・人間が読める証明、新時代の数学の教科書というライブラリ、の目標
TG集合論の上に全数学を構築していますが、私達はもっと基礎的な所から議論ができます。
Mizarの証明は人間がステップを1つずつ記述していく「宣言的（Declarative）」なスタイルで、定理の列を作る私達とは似て非なる感じです。

ACL2 は、型理論ではなく「関数型Lispの代入と書き換え」をベースにしています。
裏側で強力な一階論理的な自動推論を回すという点で、私たちの「Prover9（一階論理）へ丸投げする」という実利的なスピード感に非常に近い思想を持っています。