Goethe-Universität — Peter Pfaffelhuber: Interactive Theorem proving using Lean (and applications in basic probability)

Frankfurter Seminar - Kolloquium des Instituts für Mathematik

Ginkgo Seminar

Vorkolloquium für Doktoranden, Post-Docs und interessierte Studierende

An den jeweiligen Veranstaltungstagen wird mit dem Ginkgo-Seminar (Gingko - Grundlagen, Intuition, Neugier für und auf das Kolloquium) gestartet, einer exklusiven Veranstaltung von Doktoranden für Doktoranden, Post-Docs und interessierte Studierende.

Ziel ist es, die Vorträge "aus der anderen Ecke des Instituts" für alle Interessierten zugänglicher zu machen.

Das Vorkolloquium findet immer ab 15.00 (c.t.) in Raum 711 groß vor dem jeweiligen Vortrag statt.

Frankfurter Seminar

Mai 13 2026

16:45

Peter Pfaffelhuber: Interactive Theorem proving using Lean (and applications in basic probability)

Albert-Ludwigs-Universität Freiburg

Abstract: In recent years, formalizing mathematics using Lean as an interactive theorem prover has gained interest due to several large projects. E.g., currently, researchers work on the formalization of Fermat's Last Theorem, Carleson's Theorem from harmonic analysis, and Sphere Packing in Dimensions 8 and 24. In this talk, I will give an introduction to Lean and show what interactive theorem proving looks like for discrete probability theory. Interestingly, this sheds some light on the connection between probability spaces and random variables via category theory in action. If time allows, I will also present the formalization of some deeper results, the construction of Brownian motion.