19207219
Seminar with practice
Formal Proof Vetification
Christoph Spiegel
Comments
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
closeSuggested reading
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
20 Class schedule
Regular appointments
Mon, 2025-03-10 09:00 - 12:00
Tue, 2025-03-11 09:00 - 12:00
Wed, 2025-03-12 09:00 - 12:00
Thu, 2025-03-13 09:00 - 12:00
Fri, 2025-03-14 09:00 - 12:00
Mon, 2025-03-17 09:00 - 12:00
Tue, 2025-03-18 09:00 - 12:00
Wed, 2025-03-19 09:00 - 12:00
Thu, 2025-03-20 09:00 - 12:00
Fri, 2025-03-21 09:00 - 12:00
Mon, 2025-03-10 13:30 - 16:30
Tue, 2025-03-11 13:30 - 16:30
Wed, 2025-03-12 13:30 - 16:30
Thu, 2025-03-13 13:30 - 16:30
Fri, 2025-03-14 13:30 - 16:30
Mon, 2025-03-17 13:30 - 16:30
Tue, 2025-03-18 13:30 - 16:30
Wed, 2025-03-19 13:30 - 16:30
Thu, 2025-03-20 13:30 - 16:30
Fri, 2025-03-21 13:30 - 16:30