19207219
Seminar with practice
WiSe 24/25: 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
Die Veranstaltung findet am ZIB statt.
Tue, 2025-03-11 09:00 - 12:00
Die Veranstaltung findet heute im Raum 1.3.48, Arnimallee 14 statt.
Wed, 2025-03-12 09:00 - 12:00
Die Veranstaltung findet am ZIB statt.
Thu, 2025-03-13 09:00 - 12:00
Die Veranstaltung findet am ZIB statt.
Fri, 2025-03-14 09:00 - 12:00
Die Veranstaltung findet heute im Raum 1.3.48, Arnimallee 14 statt.
Mon, 2025-03-17 09:00 - 12:00
Die Veranstaltung findet am ZIB statt.
Tue, 2025-03-18 09:00 - 12:00
Die Veranstaltung findet am ZIB statt.
Wed, 2025-03-19 09:00 - 12:00
Die Veranstaltung findet am ZIB statt.
Thu, 2025-03-20 09:00 - 12:00
Die Veranstaltung findet am ZIB statt.
Fri, 2025-03-21 09:00 - 12:00
Die Veranstaltung findet am ZIB statt.
Mon, 2025-03-10 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.
Tue, 2025-03-11 12:00 - 16:30
Die Veranstaltung findet am ZIB statt.
Wed, 2025-03-12 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.
Thu, 2025-03-13 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.
Fri, 2025-03-14 12:00 - 16:30
Die Veranstaltung findet am ZIB statt.
Mon, 2025-03-17 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.
Tue, 2025-03-18 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.
Wed, 2025-03-19 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.
Thu, 2025-03-20 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.
Fri, 2025-03-21 13:30 - 16:30
Die Veranstaltung findet am ZIB statt.