Mathelia
Matheliaは、数学の定義・命題・定理・証明を、独自の形式言語を使って記述し、その内容を自動定理証明器によって確かめられる
数学記述環境です。
数式を入力して証明結果を得るだけでなく、数学的な説明、記号や語の導入、命題の定義、定理とその証明手順を、一冊の「book」
として順序立ててまとめられます。書かれた内容は、人が読むための数式や文章として表示されると同時に、機械が検査できる形式
へ変換されます。
Matheliaで数式を記述するための言語を「Mathel」、推論や証明を記述するための言語を「Thmel」と呼びます。.mathel ファイル
では使用するFormの種類や変数・定数・記号の綴りを宣言し、.thmel ファイルでは使用する推論方法や証明環境を指定していく構
想です。現在は、既定の default.mathel と default.thmel を読み込んで数学を書く仕組みが用意されています。
本は別の本を import でき、先に導入された語や命題、言語環境を受け継げます。また、必要な言語ファイルの読込み忘れ、二重読
込み、未紹介の語、壊れた数式などを検出し、問題の理由を示して拒否します。
証明には現在、主としてProver9を利用しています。書かれた定理と証明手順はMathelia内部で段階的に変換され、自動定理証明器
へ送られます。単に証明結果を表示するだけでなく、本の中で語や命題が適切な順序で紹介されているか、証明が定理の主張へ正し
く到達しているかを調べる「査読」の機能も備えています。
Matheliaは、数学を書くための記法、証明を確かめる仕組み、数学を本として読ませる表現を、一つの環境にまとめようとするソフ
トウェアです。
Matheliaの基本使用法
Matheliaの基本的な使い方は、数学を書く→機械に見て貰う、です。
まずbookというものに、記号の紹介や定義、定理とその証明、などを仕様に合った形にして並べていきます。
そして「査読ボタン」を押すと、機械に厳密なチェックをして貰えます。査読器により「未紹介の記号は無いか？」「証明は正しいか？」などが確かめられます。
（他のbookをimportすることはできますが）各bookは独立していなければなりません。
1つのbookは、1つの数学の自己完結な教科書になるべきです。
なお、人間用の説明を入れることはできますが、査読では無視されます。
MatheliaとAIエージェント
私達の理想像の中核は「誰もが堅牢な数学を作れること」です。
AIに伴走して貰いながら数学をbookとして組み立て、その正しさをbook査読器が支える。
これは数学の創作と検証を広く開くための基盤です。門戸を広げ、厳密さは下げません。
論文を取り込むだけで、後はエージェントがbookを作って、Matheliaの査読器がチェックをしてくれる未来を目指しています。
エージェントには「証明を作る」などの高度な作業も期待できますが、単純作業もやらせましょう。
例えば、Matheliaにはファイル名編集の機能はついていますが、自分でそれを操作するよりエージェントにやってもらう方が安全です。
他のbookにimportされていたら、それも直さなくきゃいけないので。