ATP研究会のページへようこそ！
当会では「数学のATP」の研究をしています。ATPとはautomated theorem prover(自動定理証明機)の略で、機械に数学を行わせることを目指しています。
ここでの数学とは、大学の数学科での研究対象である抽象数学です。
当会は2023年に発足し、現在数名の会員がweb上で活動をしています。
創作物はwebで公開していきますが、作りかけ・未完成が多くなるでしょう。間違いもあるかも。
コンセプト・方針
数学のめんどくさい部分は機械に任せ、その美しさに手軽に触れられるようにします。システムはできる限りシンプルにし、人間が容易に扱えるようにします。数学をweb上で構築する事の利点も生かします。
実用的なソフトを作るべく総合的に開発を進めていきます。洗練された道具で数学を形式化・機械化し、数学の美しい結果をまとめたDB(データベース)作ります。
機械での計算はいろいろなsoftwareを連動させて行わせます。その最終部分はproverに任せます。mathmaticaなどの計算ソフトや人工知能も、将来的には取り込みたいです。
現在地～目標
現在、人類の数学活動の初歩を追認できるレベルまで来ました。特に、数学の基本概念である「集合・クラス」を容易に扱う仕組みが完成しています。
数学者の相棒と言えるくらいのレベルを目指します。証明のチェックって大変らしいので、その補助ができるように。
ABC予想の懸賞金を取りに行く？定義が多くこまごましたものは、機械がやるべきです。
（私たちがやらなくても）いずれは機械が数学をやるようになるでしょう。人間には発見出来ないような定理や証明を見たいです…
御案内
当会では、一緒に研究をしていただける会員を募集しています。
数学、論理学、プログラミング、どれか得意な方はぜひ！新しい数学世界を作りたい方はぜひ！ちょっとのお手伝いでもぜひ！
「数学の教科書」で \(\blacktriangleleft\) がある定理は当システムで証明ができています。証明を見てみたいだけ、という方もお知らせください。
当会をご支援していただける方のご連絡もお待ちしております。考える葦の成長のため、何卒よろしくお願いいたします💰
代表：須田智彦[t@mshk1201.com]まで。