全学共通科目講義（１回生～４回生対象）
|
| 現代の数学と数理解析 |
| ―― 基礎概念とその諸科学への広がり |
数学・数理解析の研究の面白さ・深さを、 感性豊かな学生諸君に味わってもらうことを意図して講義し、 原則として予備知識は仮定しない。 | |
| 日時： | ２０１６年５月２７日（金） １６：３０－１８：００ |
| 場所： | 数理解析研究所 ４２０号室 |
| 講師： | 照井 一成 准教授 |
| 題目： |
コンピュータ証明はどこまでできるのか？ ---数学基礎論とコンピュータ科学基礎論の観点から--- |
| 要約： |
本講義では、コンピュータに定理を自動証明させる可能性について問題提起したい。
数学の中核にあるのが創造的活動（予想を立てたり、新概念を考案したり）であることは
間違いないが、ひとまずそれらを排して、
与えられた一群の公理から目標定理を導出する純粋に形式的な
ゲームを考えよう。この「証明ゲーム」において、
コンピュータは人間にどこまで太刀打ちできるのだろうか？
一見すると、自動定理証明の継続的発展により、将来的に部分成功することもありうるように見えるが、それは本当だろうか？一方で伝統的な数学基礎論は、ゲーデルの不完全性定理等により一定の理論的限界があると主張するが、それはどこまで現実にあてはまるのだろうか？最後にコンピュータ科学基礎論においては、「証明」は「プログラム」と同一視され、それ自体が重要な研究対象となっているが、この理論を援用することはできないだろうか？ 以上を踏まえた上で、次の問いについてごく私的な観点から論じたい。 「仮にもしも将来コンピュータ証明が成功するとしたら、それはどのようなシナリオによってだろうか？」 参考文献：
|
|
"http://www.kurims.kyoto-u.ac.jp/ja/special-02.html" | |
