Hauptinhalt

Topinformationen

Reading Club: Homotopy Type Theory

8.30504

Dozenten

Beschreibung

Course Description:

Proof assistants support mathematicians and programmers in developing formal proofs in an interactive human-machine collaboration. Recent efforts in Artificial Intelligence target at further automatizing this process by applying general problem solving strategies or machine learning. Several proof assistants, like Coq, Agda, and Idris, are based on type theory as a formal framework. Homotopy Type Theory (HoTT) is a relatively new branch of mathematics that aims at providing a solid foundation for such approaches.

In this reading club we will study the original HoTT publication [1] and discuss both, its role as a mathematical foundational framework as well as the ramifications for automated proof checking. This course does not require any specific prior knowledge, but assumes some joy in dealing with formal systems as well as a decent interest in mathematics. People with some background in type theory (e.g. the Martin-Löf version) may gain a premium membership in our club.

To succeed in this course, active participation in our weekly club meetings, including chairing sessions, is required. Meetings should be prepared by contributing to online discussions in the StudIP forum.

[1] https://homotopytypetheory.org/book/

Learning Objectives:
1. understand the fundamental concepts of Homotopy Type Theory
2. insight into mathematical practice and its foundations

Prerequisites:
* a vivid interest in formal systems and reasoning
* some prior exposition to math, though no specific knowledge is assumed

Course Format:
* weekly in-person meetings - no online option
* Tuesdays 16:00-18:00

Assessment and Grading:
* active participation in weekly meeting, including short presentations, solving exercises, chairing sessions
* active participation in StudIP forum discussions

Important Dates:
* organization meeting at Tuesday, April 15th (if you cannot join but nevertheless want to join the club, send us a message)

Required Texts and Materials or further Resources:
* https://homotopytypetheory.org/book/

Will this class be offered again/regularly?
probably not

Weitere Angaben

Ort: 50/E07
Zeiten: Di. 16:00 - 18:00 (wöchentlich) - Room 50/E07 would be great!
Erster Termin: Dienstag, 15.04.2025 16:00 - 18:00, Ort: 50/E07
Veranstaltungsart: Seminar (Offizielle Lehrveranstaltungen)