Startseite

Abstracts for Seminar on Abstract Homotopy Theory

Alternatively have a look at the program.

Directed homotopy type theory

Posted in
Speaker: 
Paige North
Zugehörigkeit: 
Universiteit Utrecht
Datum: 
Mit, 16/08/2023 - 15:00 - 16:00
Location: 
MPIM Seminar Room
Parent event: 
Seminar on Abstract Homotopy Theory

In this talk, I will describe the development of a directed homotopy type theory. The aim is to capture (higher) categories and directed topological spaces as models of the theory, and thus use it to study phenomena such as concurrency and rewriting. I will explain homotopy type theory in a way that motivates this generalization, so prior knowledge of homotopy type theory is not required.

Formalizing the ∞-categorical Yoneda lemma

Posted in
Speaker: 
Jonathan Weinberger
Zugehörigkeit: 
Johns Hopkins University, Baltimore
Datum: 
Don, 17/08/2023 - 13:30 - 14:30
Location: 
MPIM Seminar Room
Parent event: 
Seminar on Abstract Homotopy Theory

Computer proof assistants are computer programs to check the correctness of a mathematical proof. There exists a wide variety of those, and they have been used increasingly in recent decades. Notable examples include verifications of:

* Ferguson--Hales's proof of the Kepler conjecture (2003--2014, in Isabelle)
* Feit--Thompson's Odd Order Theorem, playing a central role in the classification of finite simple groups (2006--2012, in Coq)
* some of Scholze and Clausen's work on condensed mathematics, implemented as the "Liquid Tensor Experiment" (2020--2022, in Lean)

 

... back to parent event

LaTeX version

© MPI f. Mathematik, Bonn Impressum & Datenschutz
-A A +A