When
Noon – 1 p.m., Feb. 16, 2026
Where
Various proof assistants, such as LEAN4 (which is also a computer language), turn proof writing into a process with immediate feedback. This makes proof writing just as engaging and satisfying as playing a computer game. The process of creation and development of proof assistants led to new foundations of Mathematics, called Homotopy Type Theory or Univalent Foundation. In this modern view of Mathematics and Logic, topology is at the very foundation of the whole structure. We shall discuss how this view is in many ways simpler than the traditional set-theoretic foundation and try to write some proofs together.
Curious minds can try any of the games at https://adam.math.hhu.de/.