Voevodsky と証明支援システム UniMath

先ごろ亡くなったVoevodsky（僕は「ヴォヴォスキー」と呼んでいたのだが、いい加減かもしれない）の仕事の一端を紹介しようと思う。

彼は、Milner予想、Bloch-Kato予想を解くなど、代数幾何でグロタンディックが進もうとした道で、大きな業績を残した。ヴォヴォスキーの最後の仕事は、数学の基礎とコンピュータに関係していた。

彼は、数学の証明に、コンピュータを使うべきだと主張した最初の数学者の一人で、また、そのためのコンピュータによる証明支援システムのライブラリーUniMthを開発した。

GitHub: https://github.com/UniMath/UniMath
2016年9月の講演 "UniMath - a library of mathematics formalized in the univalent style" https://goo.gl/3sJr1M

数学でのコンピュータの利用は、人工知能研究の重要な一分野だ。それは、ディープ・ラーニングや自然言語処理や検索技術とは、全く異なる技術が必要になる。

なぜ、数学の証明にコンピュータが必要なのか？
かいつまんでいうと、こういうことだ。

フェルマーの定理を証明したワイルズが、謙遜して自分は「巨人の肩の上の小人だ」と言ったように、数学は、先行した無数の人たちの業績の蓄積の上に成り立っている。

もしも、ピタゴラスの子孫が生きていたとしても、ピタゴラスの定理を使うのに、彼らに著作権料を払う必要はない。また、その「証明」を自分で繰り返す必要はない。

ピタゴラスの「教団」は、いくつかの発見を「秘教」にしていたらしいのだが、少なくとも現代の数学では、情報の共有は、学問自体の前提でさえある。

ヴォヴォスキーは、興味ふかい経験をする。

2000年頃、彼は1993年に自分が発表した論文の重要な補題が間違っていたことに気づく。でも、その頃には、その論文は広く出回っていて、多くの数学者がその証明を「信じて」いた。彼が、その間違った補題なしでも、論文の結論が正しいことを証明できたのは、2006年になってからだった。

別のこともあった。1998年に共著で彼が発表した論文の証明に対して、「正しくない」という批判が出される。結論的には、彼は、正しかったのだが、彼が、最終的に、自分が正しいことを確信できたのは、2013年になってからだった。

（このあたりの経緯は、"The Origins and Motivations of Univalent Foundations" https://goo.gl/LW2Wcq に、詳しく触れられている。）

ヴォヴォスキーは、考える。「数学が、累積的（accumulative）な性格を持つのなら、もしも、そこに誤りが紛れ込むと、それも、累積する可能性がある。」

ワイルズのフェルマーの定理の1993年の証明には、誤りがあった。それが修正されたのは、1995年のことだ。

どんどん複雑化して高度化する数学の「証明」の正しさをチェックするのは難しい。数学者の「証明」が正しいという保証はないのだ！

ヴォヴォスキーは、数学の証明は、コンピュータでチェックできるプログラムの形を取るべきだと主張し、実際に、それを実行してみせた。それについては、別のポストで触れたい。

この流れは、21世紀の数学の形式を、大きく変えていくだろう。