Computer-assisted mathematics seminar

Heidelberg University, Summer Semester 2025

def fact : Nat → Nat
| 0     =>  1 
| k + 1 => (k + 1) * fact k

#check fact    
  -- fact : Nat → Nat
#check fact 5  
  -- fact 5 : Nat
#eval  fact 5  
  -- 120

theorem fact_succ (n : Nat) : fact (n + 1) = (n + 1) * fact n := 
  rfl

attribute [simp] fact_succ

Topic and goal

In this seminar, we focus on the formalisation of mathematics in an interactive theorem prover, using the Lean programming language. Our goal will be to learn what it means to write a formal proof and have the computer validate it, or even assist us with it.

Organisation

  • In the first part of the seminar, each session will combine an introduction to a particular topic regarding the use of proof assistants, followed by hands-on computer practice. Participants will be encouraged to work in pairs.
  • In the second part of the seminar, participants will work in pairs and focus on specific projects. Each team will deliver a final presentation on their project at the end of the semester.
  • Attendance is mandatory.
Date Topic
17.04 Introduction to formalisation + Lean syntax.
24.04 Propositions as types + Basic tactics.
08.05 Introduction to Git and GitHub + Logic and convergent sequences.
15.05 Dependent type theory + Intermediate tactics.
22.05 Mathlib + Advanced tactics + Choice of topics for the projects.
05.06 Tutorial / Project work.
12.06 Tutorial / Project work.
26.06 Project work (in class).
03.07 Project work (in class).
10.07 Final presentations: Isometries of the affine plane, The coin problem, Kuratowski’s theorem.
17.07 Final presentations: Polynomial functions, The coin theorem, Principal ideal domains.

Mathlib Pull Requests