「数学者とはコーヒーを定理に変える機械である」という決まり文句がありますが、別にコーヒーに限らず、何かしらを定理に変えるには『証明』が絶対に必要になります。公理から出発し、論理の糸を織り上げて定理へと至ること、それが証明です。

　証明は、ふつう日本語や英語によって書かれていますが、その背後にある論理の流れをたどってみると、独特の数理構造が浮かび上がってきます（形式的証明、証明ネット）。 実際、証明は、掛けたり割ったりできる代数構造を持っています（デカルト閉圏）。 証明は、ダイナミズムを内に秘めた動的対象でもあります（カリーハワード同型対応）。 そして証明は、有限の文字数で無限を捉えるための手段ですから、それにふさわしい位相構造を備えています（スコット位相）。

　さて、数学者とは定理を生み出す機械のことですから、証明の構造を分析し、証明をうまく見つけ出す手段を探ることによって、人工的に『数学者』をつくりだす可能性が見えてきます（定理自動証明）。 コンピュータ数学者が人間数学者を凌駕する、そんな可能性です。残念ながら、完全な定理自動証明にはいくつかの理論的限界のあることが知られています（ゲーデル不完全性、P対NP問題）。 それでも、人間数学者との協調によって限界を乗り越えることができるのではないか、そんな方向性を模索しているのが現状だと思います（証明支援系、大規模ライブラリからの定理証明）。

　本講演では、さまざまな側面を持つ『証明』について、その基礎理論の一端を紹介し、併せて『数学者をつくる』可能性について数理論理学の観点から展望を述べたいと思います。