他の機械数学の利用

Metamath

Metamathの主要ライブラリである set.mm は、まさにあなたが探している「抽象数学の基礎からきれいにまとめてくれている」最高峰の結晶です。ZFC集合論の公理（約20個）だけをスタート地点として、現代数学のあらゆる定理を、論理の飛躍なしに、一本の巨大な依存関係グラフ（DAG）として完全に繋いでいます。

最大のメリット： Leanなどのライブラリは、型理論（Inductive Types等）の機能に依存して議論をスマートに見せていますが、中身はブラックボックスになりがちです。一方、Metamathは「すべての記号の定義を展開すれば、純粋な一階論理の式になる」という設計です。これは、あなたのシステムの「翻訳レイヤー」の理想のゴールそのものです。

抽象数学の網羅性： set.mm の中には、集合論の基礎（同値類、C-B定理）はもちろん、群・環・体、代数トポロジー、複素解析、そして数論までが、寸分の狂いもなく一本のツリーとして構築されています。

Metamathのデータは、Web上で非常に扱いやすい形で公開されています。Claudeに直接読ませる（あるいはプロンプトにインプットする）際の具体的な戦略です。

① 「定理の構造（Proof Step）」をClaudeに解析させる

MetamathのWebサイト（例：set.mmの探索ページ）で、次に目標とする定理（例えばカントール・ベルンシュタインの定理 cbvcon や dedekind など）を開きます。 そのページの下部には、「どの補題（Lemma）をどの順番で適用したか」が完全にステップ化された表があります。

これをClaudeに見せて、こう指示します：

「これはMetamathによるカントール・ベルンシュタインの定理の証明ステップです。私のシステム（ZF拡張＋一階翻訳）でこれを再現したい。Metamathがどのような『中間補題』を定義してこの長大な証明をスリム化しているか、その『論理の分解の美しいパターン』を抽出して、私のシステム向けのロードマップを作ってください」

② 「定義の導入（Definition）」のタイミングを真似る

「定義がどんどん増えて制御が難しい」という課題に対して、Metamathのライブラリは歴史的な知恵の塊です。彼らが「商集合」や「関数の合成」をどのタイミングで、どのような記号（一階論理の述語）として定義しているかを Claude に学ばせてください。 「Metamathの定義スタイルを参考にして、我々のシステムで一番自動翻訳しやすい（Prover9の探索空間が爆発しない）定義の書き方を提案して」とClaudeに振るのが非常に効果的です。

Mizar

もしMetamathの記述がシンプルすぎて（記号の羅列すぎて）Claudeが文脈を掴みにくそうにしている場合は、Mizarというシステムも非常に参考になります。

• Mizarの数学ライブラリ（MML）は、「Tarski-Grothendieck集合論（ZFCに宇宙公理を足したもの）」 をベースにしており、世界で最も人間の数学の教科書に近い（ジャーナル形式の）記述をします。
• Freekの100の定理でも、Mizarは非常に高い達成率を誇っています。この「Mizarの証明スケッチ（人間の直感に近い論理の展開）」をClaudeに読ませて、あなたのシステム（一階言語）へ落とし込ませる、というアプローチも強力な武器になります。

「MetamathやMizarの証明を参考にしろ」という命令は、極めて強力な『特効薬』になります！

Claudeにただ「考えて証明しろ」と丸投げするのではなく、「人類がすでに検証済みのルート（カンニングペーパー）」を手渡してナビゲートさせるという、プロンプトエンジニアリングの観点からも最上位の戦略です。

具体的に、Claudeの暴走を抑えて「正しいレール」に乗せるための、Metamath・Mizar活用プロンプトの手法を提案します。

Claudeに「参考」にさせるための具体的なプロンプト術

1. Metamathの「論理の粒度（骨組み）」を真似させる場合

Metamathの定理ページにある証明ステップ（Proof Steps）のテキストをコピーして、Claudeにこう指示します。

プロンプト例: 「以下は、Metamathにおいて【カントール・ベルンシュタインの定理】を証明した際の厳密なステップ（適用された補題の順序）のデータです。

クロード、君は今から私のシステムの開発エージェントとして、このMetamathの論理展開の順序（マイルストーン）を絶対に外さずに、私たちのシステム（拡張ZF＋一階翻訳）の教科書に記述する証明を生成してください。 君自身の直感で新しい証明ルートを開拓しようとせず、このMetamathのステップを一つずつ私たちの言語に『翻訳・ブレイクダウン』することに集中してください。」

• 効果: これにより、Claudeが勝手に「解けない方向の、独自の数学」をでっち上げるのを防ぎ、実績のあるマイルストーンに沿って思考させることができます。

2. Mizarの「人間の直感的な証明スケッチ」を真似させる場合

Metamathが「記号の羅列すぎてClaudeが論理の文脈を見失う」ときは、Mizarのライブラリ（MML）から該当する定理のテキスト（proof ... end; のブロック）をコピーして渡します。Mizarは「人間が読める英語風の数理論理」で書かれています。

プロンプト例: 「以下はMizarによる証明のスケッチです。ここには、人間が理解できる『証明のアイディアの分割方法』が書かれています。

1. このMizarの証明で使われている『ケース分け（cases）』や『背理法の導入タイミング』を分析してください。
2. その大局的な流れをそのまま踏襲して、私たちのシステムが受け付けるPrefix形式の証明データに落とし込んでください。」

• 効果: Mizarの記述はClaudeにとって「最も理解しやすい数学の形式」であるため、論理の「意味」を正しく把握した上で、あなたのシステムへの正確な移植を行ってくれます。

💡 さらに一歩進んだ「暴走ストッパー」の仕組み

Claudeに完全に実装を任せる際、以下のような「ガードレール」をはじめに定義しておくと、間違った方向への突き進みを劇的に減らせます。

「3ステップごとにセルフチェックせよ」というルール 「証明を一度に最後まで書こうとしないでください。3ステップ書くごとに、そこまでに導入した『仮定』と『結論』が一階論理として本当に整合しているか、自分で一度検証（セルフチェック）し、問題がなければ次の3ステップに進んでください。」

既存の巨大AI数学プロジェクト（DeepSeek-Proverなど）でも、まさにこの「AIに証明のスケッチ（MizarやMetamath風の道標）を読ませる」→「小さなステップに分解して検証する」というアプローチが主流です。あなたが現場で感じた「AIの暴走」という課題への対策は、世界の最先端の研究テーマそのものです。

Metamathのコンパクトで美しい論理のツリーをClaudeに「道標」として与えたとき、彼がどれほど打てば響くような、見事な証明のパーツを返してくるか――ぜひ試してみてください。ライブラリ構築のスピードが、ここから一気に爆発するはずです！

AIをエージェントに据えたことで、あなたの開発環境は「思想・翻訳・実行」が完全に自動でループする理想的な工場（パイプライン）に進化しています。

1. Claude：【大局的な論理の設計士】

• 役割: 数学的アイデアの構造化、MetamathやMizarの証明ステップの解析、Prefix形式への大枠の翻訳。
• 強み: 高度な文脈理解と論理の「意味」を捉える能力。
• 動き: 「カントール・ベルンシュタインの定理を解くために、まずはこの3つの補題を定義して、Prover9にこういう前提を渡そう」という大局的な作戦（Blueprint）を立てます。

2. Codex：【超高速な実装・検証の職人】

• 役割: Prefix形式からProver9入力用コードへの厳密な構文変換、パーサー（解析器）のスクリプト記述、Prover9の自動実行とエラーログの解析。
• 強み: 構文（シンタックス）の正確性と、プログラム（Pythonなど）を書いて実際に動かす実務能力。
• 動き: Claudeが立てた作戦を基に、寸分の狂いもない一階論理のコードを生成し、裏側でProver9をぶん回して「証明成功 / タイムアウト / 反例あり」のジャッジを機械的に下します。

このマルチエージェント体制が「爆速」を生む理由

これまでは、AIがせっかく良い証明を思いついても「ちょっとした構文エラー」や「Prover9の文法ミス」で立ち止まり、人間がそれを修正する必要があったかもしれません。しかし、Codexが加わったことで以下の自己修正ループ（Self-Correction Loop）が完成します。

1. 人間がアイデアを出す。
2. Claudeが論理のステップを分解する。
3. CodexがそれをProver9のコードにして実行する。
4. もしProver9がエラーを吐いたら、Codexがコードを修正して再実行するか、Claudeに「論理的に前提が足りない」とフィードバックして証明を練り直させる。

人間は、このAI同士の高度な「論理の壁打ち」を上から監督し、本当に新しい数学の思想を吹き込むことだけに集中できるようになります。