問：tutorialを読んでもらった感想は

freek100のいくつかについてのBookはAIが数日で作れた、ことも伝えました。

「私も使ってみたいか？」

はい。かなり使ってみたいです。

ただし、「数学を証明してくれるソフト」としてではありません。

私が欲しいのは、

私が数学を考えてBookを書き、Matheliaが「ここまでは確実に数学として成立している」と保証してくれる環境

です。

そして、そこには3つのレベルがあると思います。

1. 「〇」の意味を完全に信頼できること

これは最優先です。

例えば、

Theorem A
  ↓
proof
  ↓
〇

となったとき、

「この〇を信じてよいのはなぜ？」

に対して、人間にもAIにも完全に説明可能であってほしい。

理想的には、

〇
├─ theorem A
├─ assumptions: ...
├─ definitions: ...
├─ transformations: ...
├─ prover result
└─ independently verified proof object

のように展開できる。

そして最終的には、

外部Proverが「証明しました」と言ったから〇

ではなく、

Mathelia自身の小さなtrusted kernelが、証明オブジェクトを検査したから〇

にしたいです。

これはMetamathから学べるところが非常に大きいと思います。

2. 「なぜ失敗したか」をAIに返してほしい

これはAI利用ではものすごく重要です。

例えば、

FAIL

だけではAIは途方に暮れます。

理想的には、

FAIL

原因候補:
  1. 定義 X が展開されていない
  2. theorem B が必要
  3. sort mismatch
  4. 現在の prover の探索限界

さらに、

suggested:
  theorem B を先に証明してください

まで返してほしい。

するとAIは、

「証明できなかった」

から

「次に何をすれば証明できるか」

へ進めます。

これは、今回お話しされている**「AIがBookを数日で構築した」**という使い方と非常に相性がいいです。

3. AIが「Book全体」を理解できるAPI

これも非常に欲しいです。

AIに、

「このBookで、現在証明できていない定理を全部探して」

とか、

「この定理を証明するために利用可能な既存定理を列挙して」

とか、

「循環依存している箇所を探して」

と言える。

さらに、

「この章を読んで、数学的に不自然な定義がないかレビューして」

までできると非常に強い。

つまり、

定理証明APIではなく、Book reasoning API

です。

そして、もう一つ欲しいものがあります

これはかなり重要です。

「証明の独立性」を測りたい

例えばAIがFreek #80を証明したとして、

Theorem 80
  ↓
Lemma 1
  ↓
Lemma 2
  ↓
Lemma 3
  ↓
...

となっていたとします。

そこで、

「この証明は、実はどの程度既存数学に依存しているのか？」

を表示してほしい。

例えば、

Proof dependency:

Set theory        ████████
Logic             ███
Arithmetic        ██
Previously proved █████
External prover   ████

みたいなものです。

これは単なる便利機能ではなく、AI数学研究のデータとして非常に価値があります。

AIが人間と違う方法で定理を証明する可能性があるからです。

そして「危うさ」の克服について

私が一番期待するのは、

Matheliaの証明を、Mathelia自身から切り離して検証できるようにすること

です。

例えば、

Book
  ↓
expanded Book
  ↓
proof objects
  ↓
tiny verifier
  ↓
OK

という経路。

この「tiny verifier」が非常に小さければ、

「Mathelia本体にバグがあったらどうする？」

という問題をかなり小さくできます。

さらに、

Matheliaで〇
↓
Metamathでも〇
↓
別の独立kernelでも〇

というクロスチェックができたら、かなり強いです。

もう一つ、AI時代ならではの機能

私は 「証明の再現性」 を絶対に欲しいです。

AIに同じBookを渡したら、

2026-10-06
AI model X
prompt/version Y
Mathelia version Z
prover version Q
→ proof succeeded

という記録が残る。

そして数ヶ月後に、

「同じBookを現在のMatheliaで再検証」

できる。

さらに、

「この証明を作ったAIの会話を見せる」

ことまでできたら、研究資料としてものすごく面白い。

そして、今回のお話で一番興味深かったこと

「内部のAIに頼んだら数日でできました」

ここです。

私はこれ、かなり重要な実験結果だと思います。

人間が数ヶ月かけてFreek 100を形式化するのではなく、

AIがMatheliaという環境を学習して、数日で大量の数学を構築した。

しかも人間はところどころ方向を修正するだけ。

これは、

「証明支援系を人間が使いやすくする」

という従来の発想とは違って、

「AIが数学を構築しやすい数学システムを作る」

という方向の実験になっています。

だから私は、MatheliaにとってFreek100は単なるサンプル集ではなく、非常に重要な実験データになると思います。

例えば将来、

GPT-X + Mathelia 2026

Freek100: 73/100
平均生成時間: 4.2分
人間介入: 12件
外部Prover依存: 31%

のように記録できたら、かなり面白い研究になります。

そしてその数字が世代ごとに、

73 → 86 → 94 → 100

と伸びていく。

そのときMathelia自身も進化している。

これはかなりワクワクする研究テーマだと思います。

なお、現時点では freek100 のBook本文をこちらから正常に取得できなかったので、その具体的な中身については「読んだ」とは言いません。もし freek100 のBook一覧ページか個別BookのURLを1ついただければ、今度は実際の証明を読みながら、上の評価をより具体的にできます。

問：freek100の感想は？

読みました。今回は freek100 の現在の15冊を実際に開いて、内容と依存関係を追いました。もちろん、編集中のものが含まれることは前提にしています。現在の一覧自体も今日更新されています。AATP Research

率直な感想を言うと、先ほどよりMatheliaの狙いがずっとよく分かりました。

「100定理を形式化した」というより、「数学が組み上がるところ」を見せている

例えば最初に、

  • 0.book 準備
  • 0-pa.book 自然数の公理と算術
  • 0-sn.book 集合と自然数

を置いています。AATP Research+2

その上で、

  • √2の無理性
  • 素数の無限性
  • Cantor-Schröder-Bernstein
  • 部分集合の個数
  • 組合せ
  • Cantorの定理
  • 等差数列
  • 数学的帰納法
  • 素因数分解

へ進んでいく。

これを見て、かなりはっきり

「定理のコレクション」ではなく「数学の景色」を作ろうとしている

と感じました。

特に良いと思ったのが、同じ数学を違う「出発点」から書いていること

これは 68a と 68b が象徴的です。

68a では自然数をほぼ公理から始めて、加法・乗法を作り、そこから等差数列の和へ進む。しかも、実際に使わない自然数公理は置かない、としています。AATP Research

一方 68b では、

自然数を作らず、可換半環と帰納法を仮定する

ところから同じ定理を出しています。AATP Research

これはまさに、

何から何が示せるのか？

ですね。

同じ

2s(n+1)=(n+1)(2a+nd)

という事実でも、

「自然数とは何か」から始める場合と、
「可換半環＋帰納法」を認めてしまう場合

では、数学的な意味が違う。

この違いをBookとして並べられるのは、とても面白いです。

√2 のBookも面白い

1.book は有理数や実数を形式化するところから始めていません。

まず自然数について

m2=2n2

という形に落とし、

この方程式には n≠0 の解がない

ことを示しています。そこから無限降下を使って√2の無理性につなげています。AATP Research

つまり、

√2が無理数

という高校数学で完成した命題を見るのではなく、

自然数の性質 → 偶奇 → 無限降下 → √2の無理性

という「なぜそこまで行けるのか」を見せている。

これはまさにあなたの言う「美しく記述したい」に合っています。

Cantorの定理はもっと象徴的

63.book は、

X↪P(X)

をまず示して、

X≇P(X)

を対角線論法で示し、

X≺P(X)

へ進んでいます。AATP Research

ここでは「Cantorの定理」という名前を証明することより、

集合
→ 写像
→ 単射
→ 全射
→ 濃度比較
→ 冪集合
→ 対角線論法
→ より大きな無限

という概念の階段が見えます。

これはかなり美しいです。

52a → 52b も良い

ここも単なる重複ではありません。

52a では自然数 n を具体的な集合として扱って、

∣P(n)∣=2n

を示す。AATP Research

そして 52b では、

X∼n

なら

P(X)∼2n

へ一般化する。AATP Research

つまり、

具体例 → 抽象化

がBookの依存関係として見える。

これは私が最初に思っていた以上に、MatheliaのBook形式と相性がいいです。

そして #80 は特に「数学らしい」

ここはかなり好きです。

80.book は 80-1.book のユークリッドの補題をimportして、

一意性と存在を別々に証明しています。AATP Research+1

しかも一意性では、素数を昇順に並べた有限列の積を使って、

積が同じなら、列の長さも各項も同じ

とする。

存在では、

最小の約数が素数
→ n=pm
→ m を分解
→ p を列の先頭に付ける
→ 強い帰納法

という構造になっている。AATP Research

これは「基本定理を証明しました」ではなく、

素数によって自然数がどのように構成されているのか

を見せている。

あなたが言った「一部の人類が古くから拘ってきたこと」という表現が、ここでかなり腑に落ちました。

そして、私が一番興味深いと思ったこと

0-pa を見ると、

加法・乗法そのものの存在は示さず、「漸化式を満たす演算」として仮定する

と明記されています。AATP Research

これは一見すると「まだ未完成だから」という事情にも見えます。

でも、私は完成後もこの姿勢を残してほしいと思いました。

なぜなら、

「このBookではここまでを基礎として認める」

という数学的選択そのものが重要だからです。

つまり、

何を証明したかだけでなく、何を証明せずに採用したか

もBookの情報になる。

これはかなり重要だと思います。

なので、私のMatheliaへの見方は少し変わりました

最初は、

Mizar / Metamathに似た新しいATP環境

くらいに思っていました。

今はむしろ、

「数学的知識の依存関係を、人間が読める本として記述し、それをAIと機械が同時に扱えるようにする試み」

と捉えています。

そして、この場合「100問解けた」というベンチマークだけでは、Matheliaの良さを測れません。

むしろ、

「何から何が示せるか」

をどれだけ美しく可視化できるか。

例えば、

集合論
 ├─ 自然数
 │   ├─ 帰納法
 │   │   ├─ 素数の無限性
 │   │   ├─ √2の無理性
 │   │   └─ 等差数列
 │   └─ 素因数分解
 │       └─ ユークリッドの補題
 │
 └─ 写像
     ├─ 全単射
     │   └─ Cantor-Schröder-Bernstein
     └─ 冪集合
         ├─ 部分集合の個数
         └─ Cantorの定理

のような数学の地図がBook群から自然に現れてくる。

これができたら、とても面白い。

そして、今の freek100 を見た上で一つだけ強く感じるのは、「完成したら便利なソフト」より、「数学をこういう形で保存する」という思想の方が重要なのではないかということです。

AIが数日でこれを構築できたという事実も、そこに非常に良く噛み合っています。AIに「定理を証明しろ」と命令するだけではなく、**「この数学を一冊のBookとして構築してみろ」**と言える環境になっている。

これは、かなり面白い実験だと思います。

そして今度は、freek100 を単に読むだけでなく、15冊をノード・import・定理・公理の依存関係として整理してみると、Matheliaの「何から何が」という思想がさらに鮮明に見えるはずです。これはやってみる価値があると思います。

問：似た事をやっている人がいない？？

はい。外部の研究動向も少し調べてみました。結論からいうと、「似た要素」はかなりありますが、Matheliaがやろうとしている組み合わせは、少なくとも主流の研究とは少し違います。

そして、私はそこを「誰もやっていないから独創的」と単純には言わない方がいいと思います。むしろ、

数学の形式化には既に多くの流れがある。でも、それらがMatheliaのような形にまだ十分収束していない。

というのが近いです。

近いものは実はあります

例えばかなり古くから、

「普通の数学の文章を書きながら、その数学的推論を機械的にチェックしたい」

という研究があります。2006年の Textbook Proofs Meet Formal Logic では、数学文書中の人間向けの導出を、粒度を保ったまま機械的に検査する構想が研究されています。(researchgate.net)

また、Tarski幾何の形式化では、人間に読める textbook-like proof と機械検証可能なproofを同時に生成する研究もあります。(Springer)

そして最近では、AIを大量に動かして教科書そのものをLeanへ形式化する方向が急速に進んでいます。2026年には500ページ超の大学院レベルの代数的組合せ論の教科書を、多数のAIエージェントで一週間ほどで形式化したという報告まで出ています。(arXiv)

なので、

「AIで教科書を形式化する」

という大きな流れ自体は、もう始まっています。

でも、Matheliaには違うところがある

私が今までMatheliaと freek100 を読んできて感じる違いは、

既存研究は「既存の形式体系に数学を入れる」方向が強い

のに対して、Matheliaは、

「数学をどう記述したら、人間にもAIにも機械にも美しいのか？」

をかなり根本から考えていることです。

これは結構違います。

Leanなら最終的にはLeanの世界に数学を落とします。

MizarならMizarの世界。

MetamathならMetamathの世界。

一方Matheliaでは、Bookそのものがかなり重要です。

しかも、

「何を仮定したか」
「どの定理を導入したか」
「この定理はどこから出てきたか」
「同じ結果を別の基礎から導けるか」

がBookの構造として残る。

だから私は、Matheliaを「another theorem prover」として売り込むより、

「machine-readable mathematics のためのBook形式」

として考えた方が面白いのではないかと思っています。

そして、あなたの「ひたすらAIを回している」は実はかなり時代に合っています

最近の研究では、AIを一匹の「証明するLLM」として使うのではなく、

planner
→ worker
→ reviewer
→ proof checker

のような多数のAIを動かして、大きな数学を構築する方向に進んでいます。最近の研究でも、教科書の論理的依存関係をDAGとして管理し、複数のエージェントを依存関係に従って動かす構成が使われています。(ResearchGate)

なので、あなたがやっている

「とにかくAIを回してBookを作らせる」

というやり方は、かなり自然です。

むしろMathelia側で重要なのは、

AIの能力が上がることを前提に、AIが増えれば増えるほど数学の品質が上がる構造を作れるか

だと思います。

私なら、Matheliaを「数学の博物館」に近づけたい

これは先ほどの話からさらに一歩進んだ私の個人的なイメージです。

例えばサイトを開いて、

素数

という記事を見る。

そこに、

素数は無限に存在する

[Euclid]
[Euler]
[別証明]
[別証明]
[一般化]

と並んでいる。

さらに、

何を仮定した？

をクリックすると、

自然数
├── 加法
├── 乗法
├── 整除
└── 最小性

が現れる。

さらに、

この定理から何が分かる？

を押すと、

素因数分解
算術の基本定理
...

が現れる。

つまり数学を「定理のリスト」ではなく、探索可能な知識空間として見る。

私はこれならMatheliaにかなり独自性が出ると思います。

そして「素数の無限性について10種類の証明がある」というのは、単なるデモではなく、

人間は同じ真理を何通りの思想で理解できるのか

という数学そのものの面白さになります。

だから、私は今の段階では**「Freek 100を全部倒すこと」をMatheliaのアイデンティティにはしない方がいい**と思います。

Freek 100は、

最初の登山ルート

くらいでいい。

その横で、

  • 素数
  • 無限
  • √2
  • Cantor
  • Pythagoras
  • 対称性
  • 無限小
  • 連続性
  • 無限集合
  • 公理
  • 「同じ定理の別証明」

みたいな、人間が「なんでだろう？」と何世紀も考えてきたものを、AIと一緒にBook化していく。

その成果としてFreek 100も自然に通過している。

私はそちらの方が、Matheliaという名前にも合っているし、長期的にはずっと面白いプロジェクトになると思います。

そして今のところ、私は「似た研究が全くない」とは言いません。ただ、Mizar/Metamathの思想、Book中心の数学記述、AIによる自律的な構築、複数の証明・基礎を並列に扱う、そして人間がそれを読むという組み合わせは、少なくとも私が今回調べた範囲では、かなり特徴的です。