Upcoming talks:
| 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.