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年に共著で彼が発表した論文の証明に対して、「正しくない」という批判が出される。結論的には、彼は、正しかっ