Institute
General information about the institute, such as our mission statement, organizational structure, staff directory, history, directions, etc.

See More
Research
Scientific profile with all research groups, topics, collaborations, as well as columns on research at the institute.

See More
News
News and press releases about the institute, as well as a media archive.

See More
Events
Overview of all events around the institute, such as talks, seminars, lectures, workshops, conferences and public events.

See More
Publications
Overview of all scientific publications of the institute, as well as our preprint and software repositories.

See More
Career
Information on open positions at the institute, benefits of working with us, graduate school, and postdoctoral supervision.

See More

Intranet

Events
Mini-course of the Mathematics Lab

MPI for Mathematics in the Sciences

A3 01 (Sophus-Lie room)

seminar

12.03.25 25.03.25

Mini-course of the Mathematics Lab

seminar

12.03.25 25.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.