Selected topics from:

• Installation of LEAN, using the proof assistant and setting up your own project
• Fundamentals of Dependent Type Theory and Propositions as Types 
• Functional proofs and tactics 
• Basics of logic in LEAN 
• Inductive types and proofs by induction 
• Selection of well-known mathematical concepts in LEAN (set theory, integers, vector spaces, convergence, ...)
• Selection of simple proofs and proof strategies (infinitely many prime numbers, stable sets in hypercube, ...)
• The mathlib library 

For all topics, the focus is on practical work with a concrete proof assistant (e.g., LEAN).

Prerquisites: Linaer Algebra I and Analysis I

Literatur:

• The Hitchhiker’s Guide to Logical Verification von Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl und Jannis Limperg
• The Mechanics of Proof by Heather Macbeth 
• Functional Programming in Lean von David Thrane Christiansen 
• Theorem Proving in Lean 4 von Jeremy Avigad, Leonardo de Moura, Soonho Kong und Sebastian Ullrich
• Mathematics in Lean