数学におけるコンピュータの使用は、数式処理や数値計算といった「計算」
の範囲内では一定の成功を収めている。一方で「証明」の自動化は未だ覚束ない
し、「予想」や「理論構築」に至っては夢のまた夢である。また、「教育」分野
でコンピュータがどの程度の役割を果たしうるかは、職業数学者にとって大いに
興味のあるところであろう。

本発表では、数学活動の中でも特に「証明」に焦点をあて、コンピュータによる
自動定理証明の可能性について問題提起する。
依って立つのは数学基礎論における「証明論」、およびコンピュータ科学におけ
る「型理論（証明とプログラムの理論）」である。不完全性定理やP≠NP予想によ
りコンピュータによる数学の限界が示唆される現状で、あえて突破口を見出すと
したらそれは一体どこにあるのか？
近年における証明支援系（対話型定理証明システム）の発展と絡めて論じる予定
である。