Institut
Allgemeine Informationen über das Institut wie z.B. Leitbild, Organisationsstruktur, Mitarbeiterverzeichnis, Geschichte, Anfahrtsbeschreibung usw.

Mehr anzeigen
Forschung
Wissenschaftliches Profil mit allen Forschungsgruppen, Themen, Projekten sowie weiteren Forschungsrubriken des Instituts.

Mehr anzeigen
News
Nachrichten und Pressemitteilungen des Instituts, sowie ein Pressearchiv.

Mehr anzeigen
Veranstaltungen
Übersicht über alle Veranstaltungen rund um das Institut, wie Vorträge, Seminare, Vorlesungen, Workshops, Konferenzen und öffentliche Veranstaltungen.

Mehr anzeigen
Publikationen
Übersicht über alle wissenschaftlichen Veröffentlichungen des Instituts sowie über unsere Preprint- und Software-Archive.

Mehr anzeigen
Karriere
Informationen zu Stellenangeboten am Institut, Karriere Benefits, dem Graduiertenkolleg und der Betreuung von Postdocs.

Mehr anzeigen

Veranstaltungen
Mini-course of the Mathematics Lab

MPI for Mathematics in the Sciences

A3 01 (Sophus-Lie room)

seminar

11.03.25 12.03.25

Mini-course of the Mathematics Lab

seminar

11.03.25 12.03.25

Mini-course of the Mathematics Lab

- Previous Events

Previous Events


13.03.25	Florent Schaffhauser (Universität Heidelberg) : Interactive Theorem Proving in Lean IV In this mini-course, we explore the world of proof assistants and learn how to encode mathematics on a computer using Lean. The goal is to help participants develop new programming skills while becoming acquainted with formal mathematics. Each session will combine a lecture with hands-on computer practice. Practice files for each session will be provided and no prior installation of Lean is required.
13.03.25	Florent Schaffhauser (Universität Heidelberg) : Interactive Theorem Proving in Lean III In this mini-course, we explore the world of proof assistants and learn how to encode mathematics on a computer using Lean. The goal is to help participants develop new programming skills while becoming acquainted with formal mathematics. Each session will combine a lecture with hands-on computer practice. Practice files for each session will be provided and no prior installation of Lean is required.
12.03.25	Florent Schaffhauser (Universität Heidelberg) : Interactive Theorem Proving in Lean II In this mini-course, we explore the world of proof assistants and learn how to encode mathematics on a computer using Lean. The goal is to help participants develop new programming skills while becoming acquainted with formal mathematics. Each session will combine a lecture with hands-on computer practice. Practice files for each session will be provided and no prior installation of Lean is required.
12.03.25	Florent Schaffhauser (Universität Heidelberg) : Interactive Theorem Proving in Lean I In this mini-course, we explore the world of proof assistants and learn how to encode mathematics on a computer using Lean. The goal is to help participants develop new programming skills while becoming acquainted with formal mathematics. Each session will combine a lecture with hands-on computer practice. Practice files for each session will be provided and no prior installation of Lean is required.