数学のABC予想の証明論文は評価になぜ長引くのか

私が不思議に思っていることは、京都大学教授の望月新一が ABC予想を証明したとする論文が2012年にネット上に現れて以来、その証明が正しいかどうかの決着がついていないことだ。

京都大学の数学専門誌PRIMSは、2020年に論文査読が終了したということで、2021年3月の4日の電子版に論文が掲載された。PRIMS側の見解は望月の証明が正しいと確信したということだ。

いっぽう、現在、ウイキペディアの英語版では、望月の証明は証明になっていないという見解が書かれている。

物理では、実験で決着のついていない予想や理論（仮説）は いっぱいある。しかし、数学は、他の学問分野と異なり、実験もいらず、論理だけで正しいかどうかが示されると、私は思っていたので、この長びく評価にびっくりしている。

数学の証明は、ゆるされる推論規則で、仮定された命題から予想の命題を導くことである。実際には、その証明の過程をつぶさに書くとあまりにも膨大になり、だれでも推論できると思われるものは飛ばす。いっぽう、査読する側は、また、論文の簡略化への自分の基準をもっていて、その飛躍をとがめる。論文投稿者と査読側との争いの結果、読みやすい適切な長さの間違いのない論文が出版される。

この査読過程で、証明の飛躍部分で、反例が見つかれば、その証明は明らかに誤りである。しかし、数学の予想自体はいまだ反例が見つかっていないものであるから、証明の飛躍部分に反例を見つけるのは一般にはむずかしいことが多い。出版されてから論文の証明が誤りだったということが判明したことも 歴史上 幾度もあった。

したがって、査読に１、２年かかるのは不思議ではないが、今回はそれでも長い。査読をする研究者も大変だろうと思う。

コンピュータが証明を考えだすのはむずかしいだろうが、人間が与えた証明の飛躍点をコンピュータが指摘するのは比較的容易ではないか、と私は思った。そのためには、コンピュータが人間の書いた証明を、コンピュータが扱える形式言語に変換すればよいのだ。ここで、ディープランニング型のAIが使えるのではないか、と思った。

そう思って、最近、数理論理学やゲーデルの定理についての本を読んでいるが、どうも命題の扱いが思いのほか、理解しがたく、コンピュータが数学の証明の判定に役立つか否かに自信を失いつつある。なんか、ゲーデルの不完全性定理の証明も納得がいかない。形式言語の枠を超えている。

もしかしたら、AIはあくまで統計的判断の高速大量実行の手段であって、真理を扱う分野や、誰かの人権に関係する分野を扱うには不適切なのかもしれない。AIは間違ってもかまわないという考えにもとづく。