ATP研究会のページへようこそ！
当会では新時代の数学の研究・開発をしています。
ここでいう数学とは、大学の数学科で扱われるような抽象数学を指します。
当会は2024年5月に正式発足し、当初は「数学のATP（Automated Theorem Prover）」のやろうとしていました。
現在数名の会員が主にweb上で活動をしています。
成果物は順次公開していきますが、開発途上のものや不完全な部分も含まれます。
2026年4月からはAIの利用を開始しました。
MatheliaとAI
私たちはMatheliaという「数学作成のためのソフト」を開発しています。
「多様な数学表現」から「定理の完全な証明」までを可能にした、操作の簡単なソフトを作ろうとしています。
「美しく堅牢な数学」を築くための最良の道具を。
MatheliaではBookというものに数学を作成します(チュートリアルも、Bookとして書かれています)。
Matheliaの基本的な使い方は、数学を書く→表示を確認する→機械に見て貰う、です。
できた数学を鑑賞するのは人間ですが、このソフトを使って数学を作るのはAIになるでしょう。
MatheliaはAIにも使ってもらうことを最初から念頭に置いています。
AIはチュートリアルやいくつかの例を見れば、すぐに仕様を理解しMatheliaを使えるようになるはずです。
御案内
当会では、一緒に研究・開発に取り組んでいただける会員を募集しています。
今後、大学の数学科の仕事は大きく変わるはずです（私たちがやらずとも…2030年代にはまず論文の査読が機械に代わられるでしょう）。ともに成し遂げませんか？
型理論の制約に窮屈さを感じている機械数学研究者の方へ。ここなら本物の数学の自由な構築ができます！？
新時代の数学をいち早く体験したいという方も大歓迎です。
Matheliaは無料でアカウント登録するだけで使用できます！どんどん使って（できれは開発のための建設的な意見を）下さい～
当会の活動をご支援いただける方からのご連絡もお待ちしております。
代表：須田智彦[t@mshk1201.com]まで。