コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-

で、人工知能というわけではないのだが、こないだ「400年をかけたケプラー予想の解決は、コンピューターの力も証明した « WIRED.jp」なんてな記事を読んだせいもあって、なんとなく気になっていた証明支援系に関係ありそうな本を本屋で見かけたので買ってみた。

これが当たりで、ヒルベルトの形式主義の話から、ゲーデルの不完全性定理、チューリングマシンによる「自己証明するプログラム」の話などが一つの流れとして書かれていて、そこに「P対NP問題」がからんできて・・・という感じで非常に面白い。そして最終章では形式主義から導かれる証明支援系の話から、HOLなどの証明支援系プログラム言語の可能性、さらには数学定理の機械学習と人間との協働へと話は広がっていく。

うん、面白い。なんか関数型プログラミング言語勉強したくなった。OCamlとはHaskellとかの解説書買ってみるかなあ。やっぱりこれか？これなのか？