『コンピュータは数学者になれるのか？』照井一成｜感想
職種としてエンジニアを選ぶにあたり、コンピュータサイエンスを勉強したい！とおもいたち、色々と調べていると、コンピュータサイエンスの根っこには《 ゲーデルの不完全性定理 》など、数学論理学があることを知りました。そんなとき、
このサイトを拝見し、実際に読んでみたところかなり面白い本でした。ただ、数学（特に基礎論）初学者、コンピュータサイエンス初学者の自分にはなかなかにむずかしい本でして、、すぐに忘れてしまわないようにもメモとして感想をかけたらなとおもいます。
本書の流れ
本書の目次
数学者を作ろう
対角線上に追い詰めろ
計算よ停まれ！
NPの壁
活き活きした証明
対角線方向にむかう未来
タイトルにもあるとおり、「コンピュータは数学者になれるのか？」という問いを中心として、本書は展開していきます。 またここで重要なこととして、「数学の目的は、単に真理を発見することではなく、それを定理として証明することだ」というふうに、明示的に数学の目的を設定しています。つまり、本著は人工数学者をつくりあげていく本でもありつつ、その背景としての「証明を証明しようとした数学の流れ」を中心とした内容ともいえます。
まず、数学基礎論を用いつつ、その後、カントールの集合論と対角線論法・ヒルベルト計画・ゲーデルの不完全性定理にふれ、タルスキの定理・チューリングの停止問題・ゲンツェンの無矛盾性証明、P対NP問題、カリー・ハワード対応へと、つまり「『数学と証明』から『プログラムと証明』へと」展開していきます。
感想
この本を読む前までは「コンピュータサイエンスの裏側には数学論理学があるっぽい！」というかなり曖昧だったイメージは、ゲーデルの不完全性定理などから、P対NP問題やカリー・ハワード対応などへと繋がり、実際に数学論理学（基礎論）がどうコンピュータサイエンスへと繋がっているのかを知ることができ、とても読んでよかったです
また、この本に加え、結城浩さんの『数学ガール｜ゲーデルの不完全性定理』も読んだのですが、どちらにも共通しているのは、「《 ゲーデルの不完全性定理 》はネガティブな意味で解釈されがちだが、ポジティブな面もある！そこを理解するべきだ！」といった信念でした。そこで、ゲーデルだけでなく、無矛盾性の証明を行ったゲンツェンを登場させ、「ゲーデル的な限界を認識しつつ、ゲンツェン的に突き進む」ということを主張しています（＊ゲンツェン的：できるところまでやってみよう！という下から突き上げる姿勢）。そしてそこには、大きな希望を感じました。
正直、読み応えがありすぎて、解釈しきれていない部分、またここで書ききれていない重要なことがありまくってます。何度も何度も繰り返して読みたい本です。
