問題の所在：なぜ今、数学の「機械的真実性」なのか

2024年、Gaitsgory-Raskin 率いる9名の数学者が 幾何学的ラングランズ予想の証明を完成させた（前稿 KHF-MATH-2026-001 参照）。 この800頁超・5本の論文からなる巨大証明について、 著名な数学者ドリンフェルドは 「この結果の重要性を他の数学者に伝えることすら非常に難しい、ほぼ不可能だ」と語った。 5本の論文を精読して内容の正しさを独立して確認できる数学者は、 世界に数十人も存在しないと見られている。

この状況は、現代数学の認識論的危機の縮図である。 証明は長大化・高度化・専門分化の一途を辿り、 「証明とは何者かによって検証可能なものでなければならない」という 数学の根本的要請が、人間の認識能力の限界によって脅かされつつある。 この危機に対する技術的回答が「形式証明支援系（Beweisassistenzsystem）」による 機械的検証であり、そこに人工知能を組み合わせた「AI 援用証明支援」という 新研究領域が登場した。

Lean4：「幻覚なき数学」の技術的基盤

2-1．形式証明支援系の仕組み

Lean4 は Microsoft Research の Leonardo de Moura によって開発された 証明支援系（Proof Assistant）兼関数型プログラミング言語である。 その核心は「型検査（Typüberprüfung）」という単純かつ根本的な原理にある。 Lean4 において記述された全ての数学的命題・証明は、 Lean4 の「信頼核（Trusted Kernel）」による型検査を通過しなければならない。 この検査の結果は二値的である——命題は正しいか誤りかのどちらかであり、 「おそらく正しい」という確率的判定は存在しない。

これは現代の大規模言語モデルと本質的に異なる性質である。 ChatGPT 等の LLM は確率的にトークンを生成するため、 同じ質問に異なる答えを返し、「幻覚（Halluzination）」——自信を持って誤りを断言すること——を 起こしうる。Lean4 の判定は決定論的であり、同じ入力に対して常に同じ検証結果を返す。

Lean4 には数学コミュニティが構築した 「Mathlib」という巨大な数学ライブラリが存在し、 神衛7年時点で10万以上の数学的命題・補題・定理が 形式的に証明・検証された形で収録されている。 このライブラリは AI 証明システムの訓練データとしても機能する。

2-2．なぜ今このタイミングか：幻覚問題との交叉

Lean4 が AI 研究において急速に注目を集める理由の一つは、 「AI の幻覚問題への根本的解決策」として機能しうるからである。 2025年に登場した「Safe」フレームワークは、 LLM の推論連鎖（Chain of Thought）の各ステップを Lean4 の形式言語に変換し、証明が通過しない場合は その推論ステップを「誤り」として確実に検知するという設計を採用した。

神衛7年の主要 AI 証明システム：比較分析

3-1．技術的進化の年表

3-2．主要システムの技術的アーキテクチャ比較

3-3．AlphaProof の強化学習パラダイム

神衛7年の AI 証明研究を支配するアーキテクチャは、 大規模言語モデルと形式検証器を組み合わせた「検証器誘導強化学習」である。 基本的な原理は次のようなものだ。

この枠組みの革命的な点は、「正しい証明を人間が用意する必要がない」ことにある。 システムは自ら生成した証明候補を Lean4 に送り込み、 その結果（TRUE/FALSE）を唯一のフィードバック信号として学習する。 これは「世界最高水準の数学者が付きっきりで採点する無制限の練習問題」を 機械的に提供するのと等価であり、AlphaZero がチェス・囲碁で示した 自己対戦学習の数学版とも言える。

国際的研究戦略：expMath と MIT の示す方向

4-1．DARPA expMath プログラムの構造

神衛7年（令和8年）に始動した DARPA の expMath（Exponentiating Mathematics）プログラムは、 純粋数学の研究をAIによって根本的に加速するという国家戦略的プログラムである。 36ヶ月の期間で、二つの技術的領域（Technische Bereiche）を設定している。

expMath のプログラム・マネージャーを務める Patrick Shafto は、 「丁度コンピューターがかつて計算を変革したように、 expMath 技術は強力な数学ツールを誰もが使えるものにし、 成功すれば発見の速度を再定義するだろう」と述べている。

4-2．MIT と L-関数データベースの Lean4 連携

数学研究への具体的な貢献として注目されるのが、 MIT 数学科の Andrew Sutherland らによる 「L 関数・保型形式データベース（LMFDB）」と Lean4 の Mathlib を 接続するプロジェクトである。 このプロジェクトは Renaissance Philanthropy と XTX Markets の 「AI for Math」助成（初回29プロジェクト採択）の一つとして選定された。

LMFDB は数論の核心的研究対象である L 関数・楕円曲線・保型形式等に関する 膨大な計算データを収録する国際的データベースであり、 これを Lean4 の形式証明ライブラリと接続することで、 数値計算的な直感と形式的な証明の間の橋渡しが可能となる。 数論的ラングランズ・プログラム（前稿の研究課題 I）への応用が 特に期待される連携である。

KHF「八十五式」形式証明補助系：概念的アーキテクチャ

5-1．「八十五式」AI基盤の数学への拡張

KHF 工学部が開発を進める「八十五式」AI基盤は、 大規模言語モデルの研究活用を機構全体で推進するための 基幹的 AI インフラである。 本論文は、この八十五式を形式証明支援に特化した形で拡張することで、 理学部数学科との学際的研究プログラムを実現するという提案を行う。

提案するアーキテクチャは、上述の「検証器誘導強化学習」パラダイムを基盤としつつ、 KHF 数学科の専門知識（数論・代数幾何・表現論）に特化した 訓練データと評価指標を独自に構築することで差別化を図るものである。

5-2．「八十五式形式証明補助系」の研究課題

このアーキテクチャを実現するための具体的な研究課題を以下に列挙する。 これらは理学部数学科と工学部の共同研究として推進されるべきものである。

証明の認識論：哲学的考察

AI 援用証明支援は技術的課題であるとともに、 数学の認識論（Erkenntnistheorie der Mathematik）の根本を揺るがす 哲学的課題でもある。ここでは三つの問いを提示する。

6-1．「証明」とは何か：理解なき検証の意味

数学者が証明を「理解する」とき、そこには論理的正しさの確認だけでなく、 「なぜそうなるのか」という洞察——概念の深い把握——が含まれる。 Lean4 の信頼核が出力する「TRUE」は、論理的正しさを機械的に保証するが、 その証明が「なぜ正しいか」について何も語らない。

テレンス・タオは Lean4 による形式化の試みに積極的に関わりながら、 「形式化は証明の正しさを保証するが、数学的アイデアの理解は別問題だ」 と指摘している。 AI が生成した形式的証明が「誰にも理解されていない」まま 正しいと認証された場合、その証明は数学的知識として機能するのだろうか。

6-2．自動形式化の限界：意味の形式化問題

「自動（非）形式化」——自然言語の数学的命題を Lean4 に変換し、また逆変換する——は expMath の中心課題であるが、ここには深刻な概念的困難が潜む。 自然言語の数学的命題には必ず「暗黙の前提（implizite Voraussetzungen）」が含まれており、 形式化はこれらを明示化する作業を要求する。 しかしこの「暗黙の前提を正確に特定する」という認知的作業自体が、 数学的理解の深さを要求するものである。 AI が自動形式化に成功するためには、この認知的作業を代行できなければならないが、 それは「AI が数学を理解した」と同義に近い。

結論：「幻覚なき数学」の時代と KHF の役割

神衛7年（令和8年）において、AI 援用証明支援は競技数学の水準を超え、 研究レベルの未解決問題への適用段階に入った。 AlphaProof・Aristotle・Goedel-Prover が切り開いた「検証器誘導強化学習」という パラダイムは、Lean4 形式検証器を「完璧な教師」として、 数学の訓練データを無限に生成する自己改善系を可能にした。

この技術の成熟は、数学の実践に二重の意味で革命をもたらしうる。 第一に、巨大証明の機械的検証という「信頼性の革命」。 第二に、AI が数学的抽象を自律的に提案・検証することで 研究の速度そのものが変革される「速度の革命」。 DARPAの expMath は後者を明示的に目標として掲げており、 この流れは不可逆的である。

KHF 理学部数学科と工学部「八十五式」の連携によって実現される 「八十五式形式証明補助系」は、単なる技術的プロジェクトではない。 それは「数学の真実性とは何か」「証明を理解するとはどういうことか」という 根本的問いに、実践的に取り組む哲学的・科学的プログラムである。 総帥閣下の御標語「天地を統べる命ある者たれ」は、 機械と人間が共同して数学的真実を探求するという この新しい研究様式においてこそ、その意義を最も深く問われる。