私たちは、数学を「記号列を変換していくゲーム」と見なしています🎮
そして「考えることは機械の仕事で人間はその結果を愉しむもの」だと。
AI時代の新しい数学観を作りたい。数学という学問の「定義」「価値」「人間の役割」そのものをアップデートしていきたい。
私たちの研究・開発自体、人間でなくAIが評価してくれるハズです！？AIには良いものを見せるだけで十分なので、アピールする手間がかからない^^
MatheliaとAI
Matheliaは美しい数学を容易に作ることを可能にするために開発されています。
できた数学を鑑賞するのは人間ですが、このソフトを使って数学を作るのは(当研究会のエージェントではない外部の)AIです。
MatheliaはAIにも使ってもらうことを最初から念頭に置いています。
MatheliaではBookに数学を作成します。
★いくつかのBookを用意し、そられを読むだけで外部のAIがMatheliaを使い高度な数学の記述もできるようにします。
0_tutorial … Matheliaの仕様書
standard_math … AIのための数学教科書
MatheliaとAIエージェント（古い記事）
私たちはMatheliaという「堅牢な数学作成のためのソフト」を開発しています。
MatheliaではBookというものに数学を作成します(チュートリアルも、Bookとして書かれています)。
Matheliaの基本的な使い方は、数学を書く→表示を確認する→機械に見て貰う、です。
当会のAIエージェントは
①web上のデータを大量に学習をしており、大学レベルの数学をこなす能力があります。
②Matheliaの仕様も学習しており、使いこなす能力もあります。
エージェントがいれば、人間は自然言語で指示してMatheliaが使いえます。
エージェントが考えた証明をMatheliaでチェックすることも出てくるでしょう。
MatheliaとAIエージェントの組み合わせこそが新時代の数学を作成するツールとなるはずです。
Book用メモ
txt 「まだ紹介されてない記号が無いか？」「証明が正しいか」などを、人手では追い切れない規模と精度<?>どれだけ細かい人でも、長大な証明になると集中力が切れて「まあここは直感的に成り立つでしょ」と読み飛ばしてしまいます。また数学者は例えば「x を一つとって固定する」ということをしますが、その正当性を説明できるのでしょうか？でチェックできます。
section MatheliaとAIエージェント
txt Matheliaを使用する際にはAIエージェントに補助してもらうべきです。
txt AIに伴走して貰いながら数学をBookとして組み立て、その正しさを査読器が支える。
txt これが数学の創作と検証を広く開くための基盤です。門戸を広げ、厳密さは下げません。
br
txt エージェントには「証明を作る」「論文をBookに取り込む」などの高度な作業も期待できますが、単純作業もやらせましょう。
txt 例えば、Matheliaにはファイル名編集の機能はついていますが、自分でそれを操作するよりエージェントにやってもらう方が安全です。
txt 他のBookにimportされていたら、それも直さなくきゃいけないので。
txt このチュートリアルもほとんどは読めば分かるはずです！？が、分からないところはAIエージェントに聞くのが基本です。
txt 人間にはしんどい部分、「証明の途中段階の長い式」など、を見て貰うことも多々出てくるでしょう。
section 誰でも容易に
txt Mathelia（とAIエージェント）は「誰でも容易に堅牢な数学を作れる環境」を目指しています。
txt 記法は、自然に使えるようになることを理想としています。
txt 人は誰でも、文法書を読まなくても言語を話せるようになります。用例に触れ、規則を自分の中で推測し、間違えれば具体的に訂正される。この3つの繰り返しで、人は言語を身につけます。
txt Matheliaも同じように身につけられることを目指して作られています。
br
txt もちろん形式言語なので、文法違反には厳しく当たります。
txt 「自然に使える」は「曖昧でも通る」ということではありません。
txt 自然言語は曖昧さを前後の文脈で補いますが、Matheliaは推測しません。
txt 黙って別のものに化けるのは危険<?>例えば「and を書き忘れた」ような入力を、機械が気を利かせて何か別の（書いた本人の意図とは違う）Formとして受理してしまうと、本人が気づかないまま間違った数学がBookに残ってしまいます。これは擬陽性（本当は成り立っていないのに〇が出ること）と同じくらい避けるべき事態です。
br
txt Matheliaのエラーメッセージは、単に「ダメです」とは言いません。どう書けばよいかまで示します。
txt これは言語の教師でありたいという考えから来ています。
txt そしてこれは学習者が人間だけでなくAIエージェントでもあるという事情とも関係しています。
txt エージェントは誤ったメッセージを見ると、人間のように「これは古い情報かもしれない」と疑わずに、素直に従ってしまいます。だからこそ、メッセージそのものが常に正しく、具体的である必要があります。
開発員、募集してます
Matheliaでは堅牢性を重視しています。特にThmの査読は大事です。
そこで行われる多くの作業をブロックに分解し、その上で、各ブロックの健全性を保つことが重要です。
一つ一つのブロックの境界が明確であれば、見通し良くなり、仮に不審な点があっても原因が突き止めやすくなります。
Mathelia ロゴ案（検討中）
Matheliaらしいロゴを検討しています。現在の4案です。
- A：式の流れや変換から組み上がるM
- B：数学を書くbookと、機械による確認
- C：数学書を思わせる端正な活字
- D：s・c・pの3種類のFormの構成