歴史～現状
機械数学の源流は1920年代のDavid Hilbertによる数学の形式化の試みに遡れます。その流れの中で一階言語・論理が標準的基盤として確立されました。これは数学のほぼ全領域を記述可能な強力な枠組みです。
「一階論理に基づくATP」も2010年頃には高い完成度に達し、proverを始めとして無料で使用できるATP softwareも登場しました。
こうした発展により、機械数学は「原理的には」実現可能であったと言えます。実際、組合せ論・論理パズル系など特定領域では非常に強力で、四色問題・Kepler予想の解決など重要な成果も生まれました。
しかし2020年頃まで、広範な抽象数学の実践にはほとんど使われませんでした。その主な理由は、一階言語に基づく記述の不便さ・煩雑さにあります。抽象数学を記述しようものならすぐに「うんざり」させられ、進展が困難だったのです。
近年、その状況は変わりつつあります。一部の数学者が機械数学に注目し、活用する動きも出てきました。例えば Terence Tao は2019年頃から、定理証明支援系への関心や、それが将来的に数学のスタイルを変える可能性について言及し始めました。また、ABC予想の証明をめぐる議論においても、機械による形式的検証の必要性がしばしば指摘されています。
とはいえ、機械数学は依然として賛否の分かれる分野です。懐疑的な数学者の見解を要約すれば、「正しさは保証されるが、コストと美しさのバランスが悪い」という点に集約されます。
近年急速に発展しているsoftwareにLeanがあります。それは従来のATPとは異なり、人間と対話しながら証明を構築していく点に特徴があります。
しかし、Leanの習得には高いハードルが存在します。素朴集合論のパラドクスを回避する方法には、一階言語による公理的集合論の他に型理論があり、Leanは後者に基づいています。型理論は（構造が明示的で再利用しやすい利点がある一方）集合論的直感と異なるため多くの数学者にとって理解が難しいです。関数型プログラミングやタクティクなどの学習も必要です。
さらに、実際に証明を形式化するには多大な労力がかかります（特にライブラリmathlibに存在しない場合、地獄）。コストに見合うリターンが得られるかについては議論があり、本質よりも手続きが前面に出るLeanの証明が数学の美しさを損なう可能性も懸念されています。
発想・アイデアを重視し、簡潔さ・エレガンスを尊ぶ従来の数学文化と、厳密さ・完全性を徹底する機械数学の文化との間には、依然として大きな隔たりがあるのです。
私たちの仕事～展望
私たちは新しい機械数学にチャレンジしています。
その最初の仕事として、一階言語・論理の拡張に着手しました。数学の基本概念である「集合」や「クラス」を自然な形で扱えるようにしたことで、数学の導入は大きく改善されたと考えています。「数学で日常的に用いられる表現や、人間にとって美しい記述を、機械でも扱えるようにする」ことを目標に、言語・論理の継続的な拡張が不可欠であると考えています。
言語・論理の実装は地道だが大事な仕事です。現在は、PHPを用いて言語処理を行い、外部の定理証明器（prover）に推論を担わせる基盤部分が完成しています。今後は、PHP自体による推論機能の実装も含め、システム全体の能力を段階的に拡張していく予定です。
また、数学の教科書を作る試みも開始しています。これは数学を基礎から再構築し、その広大な体系を機械が扱える形で記述・蓄積していくプロジェクトです。現時点では、フェルマーの最終定理に至るまでの道筋を、可能な限り簡潔かつ自然な形で整備することを一つの目標としています。その実現可能性については未知数な部分もありますが。
近年、AI技術は急速に発展しています。私たちはこれを積極的に活用すべきだと考えています。
例えば、私たちがいくら言語を拡張していっても自然言語を扱うまでになるのは不可能です。しかし、AIを用いることで、自然言語と形式言語との相互変換が現実的なものになりつつあります。（なおこの文章はAIにかなり添削してもらっています💦）
さらにAIは、システム開発や証明探索といった領域においても、大きな力を発揮することが期待されます。
（私たちがやらなくても）今世紀中には、数学という営みの多くは機械によって担われるようになる可能性があります。数学的主張の正しさは、個々の数学者ではなく、機械によって検証されることが標準になるかもしれません。また、人間の直観や想像力に相当する能力についても、いずれ機械が人間を上回る可能性があります。
そのとき数学は、実用的な営みであると同時に、人間にとっての知的な楽しみとしての側面をより強く持つようになるでしょう。人間には到達できなかった定理や証明が発見される未来も、決して遠くはないのではないでしょうか。