機械数学の歴史
源流は1920年代のHilbertによる数学の形式化に遡れます。彼は当時すでに完成していた一階言語を使いました。それは数学のほぼ全領域を記述できます。
「一階言語のATP」も2010年頃には完成しています。proverを始めとして無料で使用できるATP softwareもあります。だから機械数学は「原理的には」出来ていると言えます。四色問題の解決など一定の成果もあります。
しかし2020年頃の状況では、抽象数学において機械はほとんど役に立っていません。どの研究も、一階言語による数学の記述にうんざりさせられて進展が見込めない結果に終わっているようです。一階言語では表現力が弱すぎするのです。
数学のルール作り
私たちの機械数学へのチャレンジに当たって最初の仕事は「数学でよく使用される表現、ヒトにとって美しい記述を、機械に取り扱えるようにする」事でした。私たちは一階言語の拡張をし、いろいろな表現の変換規則も作りました。特に数学の基本概念である「集合・クラス」を自然な形で使えるようにしたことは、数学の出だしをスムーズにしたと思います。
さらに「定義とは何か」を定義したり、数学者の行う証明で使われる用語まで機械に教える準備をしました。
これらの結果は数学のルールとしてまとめられています。
なお、機械には意味を訴えることはできないでしょうし、自然言語の使用も想定できません。ルールはあくまで機械のためにあり、機械が処理可能かどうかを基準に作られています。
これからの仕事
１。数学の教科書、DB（データベース）
人間用の教科書を機械用に書き換えて、登録していきます。現代の数学は枝葉が大量に伸びている状態ですが、大事な分野・重要事項のみを選び、なるべくスマートな道を通していきます。将来的には捨て去ったものも拾っていくかもです。
２。数学の処理、特に推論
phpのコードを書く事がメインです。phpはシステムの随所で使用され、例えば教科書を表示するときにDBとの連絡を行っています。推論の最終部分はproverに任せますが、mathmaticaなどの計算ソフトや人工知能も、将来的には取り込みたいです…
機械の数学能力
基礎能力として、記憶力や計算力では人間を圧倒ししかも間違いを起こしません。記号とか定理をたくさん暗記させられるし、記憶へのアクセスも瞬時にできます。\(\pi\)の計算は人間なら1000桁とかがせいぜいでしょうが、100兆桁まで行っています。ただ、少し高度なことをやらさせて計算量が爆発してしまうとフリーズしてしまうということもあります。
当システムは抽象数学の初歩を追認できるレベルです。数学者の相棒と言えるくらいにはならないと。証明のチェックって大変らしいので、その補助ができるように。ABC予想の懸賞金を取りに行く？定義が多くこまごましたものは、機械がやるべきです。
（私たちがやらなくても）今世紀中には、数学という仕事もAIに奪われるでしょう。数学の正しさは、偉い数学者達ではなく、機械が判定するのが真っ当です。人間の直観や想像力に当たるものも、人間から学習をしていずれは超えていくでしょう。早く、人間には発見出来ないような定理や証明を見たいです…