全学自由研究ゼミナール　(証明と計算機)　(証明と計算機)

アリストテレスは「ニコマコス倫理学」で、「主題に応じて厳密さの程度を使い分けることは、教養ある人間の証であり、数学でいい加減な証明を認めるのは、修辞学に厳密性を求めるのと同じくらい愚かなことである」と言った。

しかし、数学における「厳密な証明」の概念は時代とともに変化している。現時点で最も厳密だと考えられている概念として形式的証明(formal proof)があるが、高度な厳密性の代償として、自明に思われる主張の証明も長大なものになる。従って、数学をこのレベルで厳密に記述するには、計算機の使用がほぼ不可欠になる。

このゼミナールでは、計算機を用いた形式的証明について学ぶ。