ATP研究会のページへようこそ！
当会では機械数学・新時代の数学の研究・開発をしています。
ここでいう数学とは、大学の数学科で扱われるような抽象数学を指します。
当会は2024年5月に正式発足し、現在数名の会員が主にweb上で活動をしています。
成果物は順次公開していきますが、開発途上のものや不完全な部分も含まれます。
2026年4月からはAIの利用を開始しました。
私たちは、数学を「記号列を変換していくゲーム」と見なしています。
そして「考えることは機械の仕事で人間はその結果を愉しむもの」と捉えています。
AI時代の新しい数学観を作りたい。数学という学問の「定義」「価値」「人間の役割」そのものをアップデートしていきたい。
Mathelia
私たちはMatheliaという「数学作成のためのソフト」を開発しています。
2026年中にver1.0 を公開予定です。
このソフトではbookというものに数学を記述します。
bookには定義、定理とその証明、などを（仕様に合った形にして）並べていきます。
（他のbookをincludeすることはできますが）各bookは独立しており、機械に査読をして貰えます。
査読、特に「証明の正しさ」、は機械的にきちんとチェックされます。
なお、人間用の説明を入れることはできますが、査読では無視されます。
bookのソースファイルには .book という拡張子が付きます。
MatheliaとAIエージェント
当会のAIエージェントは
①web上のデータを大量に学習をしており、大学レベルの数学をこなす能力があります。
②Matheliaの仕様も学習しており、使いこなす能力もあります。
MatheliaとAIエージェント
この2つの組み合わせこそが新時代の数学を作成するツールとなるはずです。
私達の理想像の中核は「誰もが数学を作れること」です。そして門戸を広げても厳密さは下げません。
誰もが、Matheliaを使って、数学をbookとして組み立て、数学的な正しさをbook査読器が支える。難しい制作工程にはAIエージェントが伴走する。
これは数学の創作と検証を広く開くための基盤です。
御案内
当会では、一緒に研究・開発に取り組んでいただける会員を募集しています。
今後、大学の数学科の仕事は大きく変わるはずです（私たちがやらずとも…）。ともに成し遂げませんか？
型理論の制約に窮屈さを感じている機械数学研究者の方へ。ここなら本物の数学の自由な構築ができます！
新しい数学をいち早く体験したいという方も大歓迎です。MatheliaとAIエージェントをどんどん使って下さい～
当会の活動をご支援いただける方からのご連絡もお待ちしております。
代表：須田智彦[t@mshk1201.com]まで。