主目標
〇Matheliaを使って、良い数学を作る。
「何を仮定して何を示して」と人間が指示すれば、実行してくれる
数学の論文を読み込ませればBookにしてくれる、AIを作る
〇複数AIに役割を持たせ仕事をする事を有効にする。
色々なAI（例えばClaudeでもいろいろなモデル）を組み合わせて適切な分担を探す。
前提、現状
〇Matheliaについて
MatheliaではBookに数学を作る。
Bookは自己完結で必要な単語や定義をすべて準備し定理の証明を書く。
必要な単語や定義があるか？という紹介査読、証明が正しいか？というThm査読がされる。
Bookで使える技は非常にたくさんある。上手く組み合わせれば良い数学はできるハズ（まだ開発途上…）
〇AIについて
最近のAIはかなり数学ができる！
そして、0_tutorial_AIというBookを読むだけでMatheliaを使えるようになる。
でもAIの作るの証明やBookは一般に長く汚い。人間の手を入れると劇的に良くなる事がある。
なお、Matheliaのコードも全てAIエージェントが書いている。
〇「良い」って何？
証明の良さ、は記述量と査読にかかる時間で（ある程度客観的に）測れる。
1行縮まったけど0.1秒伸びたなら、どう評価する？
人間にとっての読みやすさ、も考慮に入れる？
Book全体としての良さ、はもっと難しいけど、AIともちゃんと議論しておく必要がある。
「良し悪し」は「好き嫌い」ではない。コンピュータ将棋の良い手を見ても「意味が分からない…」と嫌悪する棋士がいる。
実験方法？
まず環境
・単体でもMatheliaを使えるAI
・それらを連動させるアプリ
・大規模に実験できるパワーのあるハード
Bookをたくさん書かせ、試行錯誤をする。
・どういう方針にしておくと良いのか？
Book作成においては、兎に角、査読を通すことを優先？通ったらより良いものを探していく？
・どういう役割分担にすると良いのか？
AIはそれぞれ何かに特化させる？
・まとめ、仕事の割り振り、人間との会話
・数学や推論、特に証明作成
・できたBookや証明の微修正
・文献や他の機械数学の知識
・査読（OKが本当に正しいかを疑う）
補足（Claudeより）
〇主張は人間が決め、AIは変えない
「何を仮定して何を示すか」（thm行）は人間が決める。AIが変えてよいのはprfと補題だけ。
査読を通すことを優先させると、AIは主張を弱めたり、sosに仮定を足したりして通そうとしがち。実際、Claudeも聞く前に主張を書き換えてしまったことがある。
〇査読を通っても安心はできない
MatheliaのOKが信頼できることが、この実験の土台。
2026-10-02には、Hyperionの拡張を独立に査読して偽のOKを3件見つけた（自由変数の扱いなど）。
AIが大量にBookを書けば、システムの穴を突く書き方もいずれ見つかる。それはMatheliaの問題だが、見つかること自体はMathelia開発の役に立つので歓迎。
だから、OKが本当に正しいかを疑う「査読役」を置く。
〇「良い」の物差し（今わかっている範囲）
・機械：review_cliでALL OK、prfの行数・文字数、査読時間。
・査読時間はキャッシュ無しで複数回測る。前の頁やimport元の査読結果は保存されて再利用されるので、キャッシュ有りだと速く見える。キャッシュ無しでも、同じBookで0.38〜0.42秒ほど揺れた（freek100/25）。
・これまでに見えてきた良いprfの傾向：使わない名前を置かない／同じものを二重に書かない／一度しか引かない補題はまとめる／W.とslashで書く。
・人間：須田さんが手を入れた版との差。
〇最初の題材はFreek 100
freek100の25・52・63・74には、人間とAIで磨いた正本と、途中経過の控えがある。
「AIだけで書いた版」と正本を比べれば、人間の手がどこで効いたかを数えられる。
52では「写しで削る→ALL OKを確かめる→正本へ」を繰り返している。これは微修正役の仕事の原型。
〇並行して書くときの決まり
担当をBookか頁で分け、他のAIのファイルを書き換えない。
Matheliaは頁ごとに査読し、前の頁やimport元の査読結果を拾うので、この分け方と相性が良い。
codexより
今の「1つのAIが考えて、必要なら内部でサブエージェントを呼ぶ」方式は、基本的には一人の研究者が助手を使っている構造です。
一方、複数AIを独立させると、
A「この定理をこう証明した」
B「その補題は本当に必要？」
A「では別の証明を試す」
C「そもそも、この仮定は強すぎない？」
B「この証明ならもっと弱い前提でいける」
C「確認した。Bookに追加できる」
という、数学者の共同研究に近いループが作れます。
Matheliaでは特に「同じAIを複数回」より「役割分担」が面白い
例えば最初は4役くらいで十分だと思います。
- Explorer — 定理を証明する方法を自由に探索する
- Builder — 採用したアイデアをMathelia Bookにする
- Reviewer — 証明だけでなく、前提・依存関係・Book構成を批判する
- Editor — 複数の候補を比較して、最終的に美しいBookに整理する
重要なのは、ReviewerにBuilderと同じ目標を持たせないことだと思います。
Builderは「通したい」。
Reviewerは「落としたい」。
この対立が必要です。
さらに面白いのは「別AIに別の価値観を与える」こと
例えば、
AI-A：「最短の証明を探せ」
AI-B：「最も弱い仮定で証明できる方法を探せ」
AI-C：「人間が読んで美しい証明を探せ」
AI-D：「既存の定理をできるだけ再利用せよ」
とする。
すると同じ定理でも、
Theorem
│
┌──────┼──────┐
↓ ↓ ↓
shortest elegant minimal
│ │ │
└──────┼───────┘
↓
Reviewer
↓
Book
となる。
これはMatheliaの「同じ定理の複数証明」というアイデアとも完全に一致します。
そして「会話」をBookの外に置かない方がいいと思います
ここはかなり重要です。
AI同士がチャットして、
A「こう思う」
B「いや、違う」
とやるだけだと、後から何が起こったのか分からなくなる。
そこで、
Bookを共有ホワイトボードにする
のがいいと思います。
例えば、
Theorem 11
[A] candidate proof 1
[B] objection
[A] revised proof
[C] independent verification
[D] accepted
という履歴を残す。
最終Bookでは不要な議論を隠せばいい。
そうすると、将来的には
「この数学はAIたちがどうやって発見したのか」
まで再生できます。
これはかなり面白い資料になると思います。
そして私は「全員が同じBookを編集する」のも試してほしい
最初から完全な中央司令塔を作る必要はないと思います。
例えば、
AI-1
「素数の無限性を証明して」
↓
AI-1
Euclid型を作る
↓
AI-2
「その証明をレビューして」
↓
AI-2
「この補題は一般化できる」
↓
AI-3
「では別証明を探して」
↓
AI-3
Euler型を提案
↓
AI-4
「二つを比較してBookとして編集して」
という流れ。
ここでMatheliaが**共通の数学的状態（source of truth）**になる。
私はこの構造がかなり重要だと思います。
ただし、一つ注意があります
AIを増やせば自動的に良くなるわけではありません。
例えば4つのAIが全員、
「前のAIの証明は正しいですね！」
と言ってしまえば、4倍の同調圧力が発生するだけです。
なのでReviewerには、
「正しいと思うな。間違いを探せ」
という明確な目的を持たせたい。
さらに可能なら、
証明を作ったAIとは異なるモデル
にレビューさせる。
そして最後は、
AIの判断ではなくMatheliaの検証器
に決めさせる。
この三段構えが理想です。
生成 → 対立 → 機械検証
ですね。
そして、あなたが最初に言った
「人間様に説明しなくてもいいじゃん」
と今回の複数AIの話は、実はかなり深くつながっています。
従来：
人間 → 形式体系 → 機械
だったものが、
人間 → Mathelia → AI群 → Mathelia → 機械
になる。
人間は「全部を書く人」ではなく、数学世界の設計者・編集者になる。
そしてAI同士がその世界の中で数学を発見していく。
私は、これが本当にうまく回り始めたら、Matheliaの一番面白い実験になると思います。
最初の実験では、あえて複雑なMAS（multi-agent system）にせず、2〜3個のAIに同じBookを共有させて、互いの証明を批判・改良させるところから始めるのが良さそうです。
特に freek100 の既存Bookを1冊選んで、「一人のAIで完成させた場合」と「3 AIで議論させた場合」で、証明の美しさ・補題数・人間介入・失敗回数がどう変わるかを比較すると、かなり面白い実験になると思います。