ATP研究会のページへようこそ！
当会では「数学のATP（Automated Theorem Prover）」の研究・開発をしています。
機械に数学を行わせることを目指し、システム開発とライブラリ構築に取り組んでいます。
ここでいう数学とは、大学の数学科で扱われるような抽象数学を指します。
当会は2023年に発足し、現在数名の会員が主にweb上で活動をしています。
成果物は順次公開していきますが、開発途上のものや不完全な部分も含まれます。
2026年4月からはAIの利用を開始しました。
基本理念
私たちは、数学を「記号列を変換していくゲーム」と見なしています。
「考えることは機械の仕事で人間はその結果を愉しむもの」と捉え、常に次を追い求めています。
①機械の数学力
②人間にとってのわかりやすさ
現時点でLeanやMizarなどたくさんの機械数学が存在します。
②分かりやすさではどこにも負けないはずですが、これからも疎かにしません。
システムは初心者でもすぐ使えるよう、ライブラリは新時代の数学の教科書として使えるよう。
①数学力でもNo1を目指します。
私たちのシステムは原理的に他の機械数学を「取り込む」ことが可能なので…
ライブラリだけでなく証明AIなども？
御案内
数学を機械が扱う時代は、確実に近づいています。
機械数学は絶対にホットな研究分野です🔥
当会では、一緒に研究に取り組んでいただける会員を募集しています。
数学・論理学・プログラミング・AI利用のいずれかに経験・興味のある方、大歓迎です。
システムでの証明を見たいだけ、という方もまずはご連絡下さい。
当会の活動をご支援いただける方からのご連絡もお待ちしております。
代表：須田智彦[t@mshk1201.com]まで。