
VinhKha Le will give the math table talk next Tuesday (April 2nd). His
title and abstract are below.
Title: Why is equality like a path? HoTT takes on proofs as programs.
Abstract. Homotopy theory, in the setting of algebra and topology, is
nearly 200 years old. In that time, the field has evolved and matured a
vast library of techniques. In that time, mathematicians also realized
that those techniques could be applied to areas outside of topology. In
this talk, we will discuss homotopy theory as it is applied to type
theory, the area of logic and computer science that concerns itself
with formal systems of proofs and programming languages. This socalled
homotopy type theory (HoTT) emerged in the early 2000s partly as a
method for automated proof checking. HoTT interprets proofs of theorems
as points in spaces and proofs of equality as paths between points.
Under this interpretation, it is possible to port over techniques from
homotopy theory to resolve problems in type theory and vice versa. In
particular, HoTT can translate mathematical proofs into a programming
language such that valid proofs correspond to valid programs. A computer
can then check proofs by running the corresponding programs.
This talk will go over the general ideas of HoTT with minimal
technicality. Any details provided will be presented accessibly. No
prerequisites, though a basic understanding of proofs and programs
is suggested.
