19207219
Seminar with practice
Formal Proof Vetification
Tibor Szabo
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