トポロジー火曜セミナー

過去の記録 ~03/28次回の予定今後の予定 03/29~

開催情報 火曜日 17:00~18:30 数理科学研究科棟(駒場) 056号室
担当者 河澄 響矢, 北山 貴裕, 逆井卓也
セミナーURL http://park.itc.u-tokyo.ac.jp/MSF/topology/TuesdaySeminar/index.html

2015年05月26日(火)

17:00-18:30   数理科学研究科棟(駒場) 056号室
Tea : 16:30-17:00 Common Room
久我 健一 氏 (千葉大学)
Introduction to formalization of topology using a proof assistant. (JAPANESE)
[ 講演概要 ]
Although the program of formalization goes back to David
Hilbert, it is only recently that we can actually formalize
substantial theorems in modern mathematics. It is made possible by the
development of certain type theory and a computer software called a
proof assistant. We begin this talk by showing our formalization of
some basic geometric topology using a proof assistant COQ. Then we
introduce homotopy type theory (HoTT) of Voevodsky et al., which
interprets type theory from abstract homotopy theoretic perspective.
HoTT proposes "univalent" foundation of mathematics which is
particularly suited for computer formalization.