第2章　Matheliaの立場

2.1 数学とAI、証明支援系

2026年に入り、「AI が数学の未解決問題を解いた」「AI が大定理の証明を形式化した」というニュースが続いています。
その多くは、AI が証明を見つけ、Lean などの証明支援系で正しさを確かめるという形です。機械が正しさを保証すること自体は、もう大きな規模でできるようになりました。
一方で、そうしてできた証明は膨大な量になり、人が読んで理解するものではなくなりつつあります。数学者からは「数学で大事なのは、概念の理解と洞察だ」という声も上がっています。
Matheliaも機械が正しさを確かめるソフトですが、目指すところが少し違います。AIが作った数学を人間が見る事を強く意識しています。
そして、Lean よりは、Mizar や Metamath に近いと言えます。
Mizar の A. Trybulec は、普通の数学の文章に近い言葉で証明を書き、定理を「記事」として集めた図書館を作りました。
Metamath の N. Megill は、小さく単純な仕組みで、証明のすべての段を誰でも確かめられることを大切にしました。
彼らとは思想が似ていると感じています。彼らもAIが発達した現代に生まれていれば、このソフトのようなものを開発したかもしれません。

2.2 MatheliaとAI

Matheliaは、人間だけでなく AI も使用することを想定して作られています。AI 用の tutorial（0_tutorial_AI）も用意してあり、AI はそれを読んで Book を書きます。
人間が使うときも、分からないところは AI に聞くのが基本です。記号の意味、定理の読み方、証明が通らない理由などを、AI が Book と Mathelia の仕組みに沿って説明してくれます。
なお、例えばBookのファイル名を変更するなど初歩的な事もAIに任せるのが無難です。他のBookにimportされているかもしれないですし。

そして将来は、Book を作成するのは AI で、人間はできたものを鑑賞する、ということになる可能性が高いと考えています。
AI は定義を選び、定理を並べ、証明を探し、査読が ALL OK になるまで Book を直します。
人間は、構成や記法の選び方、証明の流れを、一冊の作品として味わいます。

美しい数学とは何でしょう？自己完結で、何から何を示しているかが分かる。隠れた前提は無く、定理の証明が正しいことは、書かれた規定のもとで機械が確かめます。
流れが完全に見えるだけでなく、しかも清らかに見えねばなりません。
Matheliaにはそのための多くの機能があります。端的な多様な数学表現を可能にしていたり、証明の細かい推論を自動定理証明器（Prover9・Vampire・Satallax）が埋めたり。
多くの機能を使いこなす事、特に証明を通す事、は人間よりAIがはるかに上手にやります。
前提を取り替えれば、別の構成の本を何冊でも作れますが、膨大な試行錯誤もAIに任せましょう。
AI の力を借りて、人が鑑賞できる数学の作品が増えていって欲しいです。

★実例がすでに多く準備されています。
2026年10月現在では、100の数学定理 のいくつかが本になっています。各本は一つの定理を目標とし、査読が数秒で終わる大きさに保たれています。