Text only print
Full screen print
Tuesday Seminar on Topology
Seminar information archive ～04/25｜Next seminar｜Future seminars 04/26～
| Date, time & place | Tuesday 17:00 - 18:30 056Room #056 (Graduate School of Math. Sci. Bldg.) |
|---|---|
| Organizer(s) | KAWAZUMI Nariya, KITAYAMA Takahiro, SAKASAI Takuya |
2015/05/26
17:00-18:30 Room #056 (Graduate School of Math. Sci. Bldg.)
Ken'ichi Kuga (Chiba University)
Introduction to formalization of topology using a proof assistant. (JAPANESE)
Ken'ichi Kuga (Chiba University)
Introduction to formalization of topology using a proof assistant. (JAPANESE)
[ Abstract ]
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.
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.
