既存のLeanやCoqといった主流派のドキュメントや解説を見ていると、どこもかしこも「型理論（Type Theory）」の難解な用語ばかりで、「なぜ、もっとシンプルに『記号の定義を展開すれば、純粋な一階論理の式（ZFC集合論の言葉）になる』という、数学本来の王道の設計にしないんだ？」と、違和感を抱いたことはありませんか？
現代のコンピュータ科学において、多くの開発者が「型理論」に流れてしまうのには、彼らなりの（数学的というよりは）「計算機的な都合」があります。
- プログラマの直感: コンピュータのプログラムは「型（Int、Stringなど）」でバグを防ぎます。そのため、計算機科学出身の形式化研究者は「数学も型で管理すれば、不条理な証明（例：\(1 \in \pi\) のような無意味な式）を未然に防げる」と考えがちです。
- 型チェックの軽さ: 型理論は、「型が一致しているか」を調べるだけで論理の正しさを高速にチェックできる（カリー＝ハワード同型対応）ため、コンピュータにとって処理が書きやすかったのです。
しかし、その代償として、数学者が黒板に書くような「自由で柔軟な数学の視点の切り替え」を犠牲にしているのが、今の主流派の限界です。
巨人の足跡：Metamath
その違和感に対し、「純粋な一階論理と集合論だけで数学を構築する」というシステムを1992年からたった一人で作り始めた男がいました。それがMetamathの創始者、Norman Megillです。彼の思想は、まさに私たちのシステムの設計思想そのものです。
- 「意味論」をブラックボックスにしない: 型理論のシステムは、裏側で複雑な「型の型チェックルール」という巨大なプログラムが動いています。Megillはこれを嫌い、「人間が検証すべきは、純粋な一階論理の記号の置き換え（代入）だけであるべきだ。すべての定義は、公理まで100%展開できなければならない」と考えました。
- 圧倒的なシンプルさ: Metamathの検証器（カーネル）は、非常に小さなコードで書かれています。なぜなら、複雑な型パズルを解く必要がなく、ただ「定義を展開して一階論理として一致しているか」を見るだけだからです。
私たちのシステムが「Prover9（一階論理証明器）」をエンジンに選んだのも、極めて論理的で正しい帰結です。一階論理まで完全に落とし込める設計だからこそ、一階論理の専門家である外部の強力なソルバーのパワーを100%引き出すことができるのです。
Metamathの思想を現代に「リブート」する
私たちのシステムはMetamathの思想を受け継ぎつつ、さらに現代的に進化しています。
- Metamathの弱点: Megillの作ったMetamathは、純粋すぎるがゆえに「人間が読み書きする記号（ASCIIコードの羅列）」が非常に無機質で、教科書を作るのが苦行に近いという弱点がありました。
- 私たちの強み: 私たちはそこに「クラスの導入」「一階言語への自動翻訳レイヤー」「LaTeXとPrefix形式の双方向処理（Web化）」を組み込み、さらに「AIエージェント（Claude）」という最強の自動記述マシンまで味方に付けています。
つまり、私たちが今やっていることは、「Metamathが証明した『集合論ベースの正しさ』を、現代のAIとWeb技術を使って、圧倒的に人間が扱いやすい形でリブート（再始動）する」という、とてつもない価値を持つプロジェクトなのです。
「世界に、同じ思想の先人がいた」ということは、私たちの進んでいる道が歴史的に検証された「正しい道」であることの証明に他なりません。
（注１）2026年7月に初めて、Geminiに色々聞いている中で、私たちの思想が孤独でないことを知りました💦そりゃいるだろ、って話ですが、全然巡り合えなかったのです。
（注２）Norman Megill氏は2021年12月9日、71歳で急逝されました（自然死とのことです）。MIT（マサチューセッツ工科大学）で計算機科学を修め、後にクロアチアのザグレブ大学で博士号を取得された、非常に情熱的な数理論理学者でした。
chatgptに聞いた
私も昔「Hilbert流の公理系から出発して数学をすべて記述しよう」と思っていたことがありました。実際にそれを実行しているとは…
それは自然な発想だったと思います。そして、実際にMetamathはそれを30年以上かけて実現してきたわけです。
Hilbert流の公理系は、一見すると非常に回りくどく見えます。
例えば、人間なら
\(P \& Q\) だから \(P\)
と一行で済ませるところを、Hilbert流では基本公理とModus Ponensだけを使って何十ステップもかけて証明することがあります。
それでもMetamathがその方式を採用した理由は、証明器の核を極限まで小さくできるからです。証明チェッカーは「置換が正しいか」「Modus Ponensが正しく適用されているか」を確認すればよく、実装が非常に単純になります。
一方、あなたの現在のアプローチは、ある意味で逆方向です。
- Metamath：「証明の最小性」を重視する。
- あなたのシステム：「証明探索の効率」を重視する。
ATPは内部でResolutionやSuperpositionなど、人間が直接書かない推論を大量に使います。その代わり、入力は一階論理でよく、Hilbert流の細かな論理定理をライブラリとして持つ必要がありません。
興味深いのは、この二つのアプローチは対立しているわけではなく、補完的だということです。
- Metamathは「この証明は本当に正しい」と厳密に検証することに長けています。
- ATPは「その証明をどう見つけるか」に長けています。
そのため、自動定理証明の分野では「ATPが証明を見つけ、最終的には小さなカーネルで検証する」という考え方が広く採られています。
あなたが以前Hilbert流から始めようと考えていた経験があるからこそ、今「一階論理は既知とする」という設計を選んだ理由もよく分かります。一度その道を考えた人ほど、論理をゼロから積み上げるコストの大きさを実感するものです。
それでも、Metamathがその困難な道を実際に歩み切り、巨大なライブラリを築き上げたことは、形式化数学の歴史の中でも非常に印象的な成果だと思います。
Metamathと私のシステムは思想は一緒ですが、アプローチはかなり違うようですね。Proverですら「人間には一瞬でわかる命題」が時間overになってしまうことがあるので、phpでも推論をするようにしています。
そうですね。お話を聞いていると、思想は近く、役割分担がかなり違うという印象です。
共通しているのは、
- 数学を厳密な形式で表現する。
- 集合論を基礎として数学全体を構築する。
- 証明可能性を機械的に扱う。
という思想です。
一方で、アプローチはかなり異なります。
- Metamathは「小さな検証器」と「人間が作る（あるいは外部で作られた）証明」を重視しています。
- あなたのシステムは「翻訳器」と「自動証明」を中心に据えています。
PHPでも推論を行っているという話は、とても納得できます。
ATPは万能ではありません。例えば、
- 定義を少し展開するだけで解ける問題
- 自明な等式変形
- 場合分けを少し整理すれば済む問題
でも、探索空間の爆発によってタイムアウトすることがあります。
そういうときに、
- 定義を先に展開する
- 明らかな書き換えを行う
- 不要な仮定を削る
- 式を正規形に近づける
といった前処理をPHPで行えば、ATPの負担を大きく減らせます。
これはコンパイラでいう「最適化パス」に近い役割ですね。
実は、こうした役割分担はATPの研究でも重要なテーマです。
証明器そのものを速くするだけではなく、
- 問題をどう前処理するか
- どんな補題を自動生成するか
- どの定義を展開するか
によって、解ける問題数が大きく変わります。
私が興味深いと思ったのは、あなたのシステムではPHPが単なる「入出力」ではなく、推論エンジンの一部になっていることです。
例えば、
数学表現
↓
PHPで構文解析、一階言語へ変換
↓
PHPで簡単な推論・簡約
↓
Prover9
↓
結果をPHPで整理という流れであれば、PHPはオーケストレーターであると同時に、「ATPに渡す前の知的な前処理」を担っています。
これは、ATPの探索を完全に任せるよりも実用的な設計だと思います。
もし今後EやVampireを試すようになっても、そのPHP側の推論基盤はそのまま活かせるでしょう。バックエンドが変わっても、「人間には明らかなことを機械にも明らかにしてから渡す」という設計思想は、どのATPに対しても価値があります。
Metamathとの対比（かなり明確）
- Metamath
→ 最小カーネル + 人間が証明を構築 - あなたのシステム
→ 意味変換 + 最適化 + ATP探索 + 後処理
つまり：
Metamath = 証明の「検証システム」
あなたのシステム = 証明の「生成・コンパイルシステム」