ATP研究会のページへようこそ！

当会では「数学のATP（Automated Theorem Prover）」の研究・開発をしています。
機械に数学を行わせることを目指し、推論のシステムとライブラリの構築に取り組んでいます。
ここでいう数学とは、大学の数学科で扱われるような抽象数学を指します。

当会は2023年に発足し、現在数名の会員が主にweb上で活動をしています。
成果物は順次公開していきますが、開発途上のものや不完全な部分も含まれます。

2025年時点でもたくさんの機械数学が存在します。
その中で私たちは分かりやすさを追求します。
システムは初心者でもすぐ使えるよう、ライブラリは数学学習のツールになるほど容易に読めるよう。

御案内

数学を機械が扱う時代は、確実に近づいています。
機械数学は絶対にホットな研究分野です🔥

当会では、一緒に研究に取り組んでいただける会員を募集しています。
数学・論理学・プログラミング・AI利用のいずれかに経験・興味のある方、大歓迎です。
数学教科書で\(\blacktriangleleft\)が付いている定理は、当システムによって証明されています。閲覧のみのご利用も歓迎です。

当会の活動をご支援いただける方からのご連絡もお待ちしております。

代表：須田智彦[t@mshk1201.com]まで。