数学のATP
「数学のほぼ全領域は一階言語で表現できる」とwikipediaにあります。「一階言語」は1920年頃には、「一階言語のATP」も2010年頃には完成しています。proverを始めとして無料で使用できるATP softwareもあります。
だから数学のATPは既に「ある程度は」「原理的には」出来ていると言えます。四色問題の解決など一定の成果もあります。
しかし現状では、抽象的数学において機械はほとんど役に立っていません。まず、数学を（機械に伝えるために）一階言語で表現しようとすると、うんざりする目に遭います。そして機械は、単純な計算では人間を凌駕しても、少し高度なことをやらさせると計算量が爆発してしまいます。「数学のATP」が乗り越えるべき壁は高いようです。
やる事
実用的な数学のATPとなるよう、総合的に開発を進めます。
数学の新しい形式化をするための理論作りから始めます。通常の数学で行われていることを明確にした上で機械でも行えるように意図します。
重要な点は一階言語・論理の拡張をして、集合に加えてクラスも扱えるようにすることです。一階言語ではTermとPropが扱われますが、私たちの言語ではTermをSetと呼びさらにClassを扱います。一階への翻訳も定めます。
略記を許容したり多様な数学表現を使えるよう枠組みを構築していきます。
理論を整えつつ、機械に実装していきます。
既知の数学定理のDB(データベース)を作ります。人類が過去に得た膨大な結果は、私たちの言語で記述されることで機械に扱える形となって保存されます。
推論はいろいろなsoftwareを連動させて行わせます。その最終部分はproverに任せます。mathmaticaなどの計算ソフトや人工知能も将来的には取り込むことを想定しています。
方針・目標
人間が楽しめるような工夫は重要です。形式化をしようとすると冗長になりがちですが、簡潔に済ませる方法を模索します。システムはできる限りシンプルにすべきです。数学のめんどくさい部分は機械に任せ、その美しさに手軽に触れられるようにしたいです。
頭の良さとしては、数学者の相棒くらいにはなって欲しいです。証明のチェックって大変らしいので補助できるように。
ABC予想の懸賞金を取りに行きます。定義が多くこまごましたものは、得意分野のはずです。
もっと発展して、数学者の仕事を奪って、大きな世界への扉を開いてくれれば…？人間には発見出来ないような定理や証明を見たい…