コンピュータは数学者になれるのか?

開催日時: 
2015/06/17 Wed 15:00 - 16:00
場所: 
RIMS420号室
講演者: 
照井 一成
講演者所属: 
京大・数理研
概要: 

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

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