Upcoming talks:
| Tue 27 Oct 2026, 16:30: Sandra Müller (TU Wien) The boundaries of mathematics - from Gödel to the study of large infinities |
| After proving that not all statements in mathematics can be proven or disproven from the accepted ZFC axioms, Gödel raised the question whether natural statements, such as Cantor’s continuum hypothesis, can be decided via extending the axiomatic framework by axioms of large infinities. While this question has been answered in the negative for large infinities, the problem of finding good axioms that decide natural mathematical statements remains open. There are several compelling candidates that we will motivate and describe, together with strong evidence for them provided by recent advances in set theory as well as their impact on other areas of mathematics. ____________________________________ Invited by Prof. Helmut Schwichtenberg |
| Theresienstr. 39, München. Room A 027 |
| Tue 15 Dec 2026, 16:30: Jasmin Blanchette (Ludwig-Maximilians-Universität München) Lean Before You Leap |
| Lean is a popular proof assistant (also called interactive theorem prover) and programming language introduced by Leonardo de Moura in 2013. I will briefly review the historical development of proof assistants since the 1960s. Then I will present Lean, Lean's Mathlib library of formally verified mathematics, and Mathlib's fast-growing AI-developed extension Tau Ceti. The talk will include a live demonstration of Lean and Mathlib. I will mention some success stories about formalized mathematics using Lean. I will conclude by describing some of my team's research on developing and using Lean. ____________________________ Invited by Prof. Gitta Kutyniok |
| Theresienstr. 39, München. Room A 027 |
All lectures are on Tuesdays at 4:30 pm in lecture hall A027 unless otherwise noticed.
Looking for past events? You may find them in the Munich Mathematical Calendar.