Mini-course of the Mathematics Lab: MPI MIS


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.

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.

Mini-course of the Mathematics Lab

Previous Events