https://studiegids.vu.nl/en/courses/2025-2026/XM_0167The course introduces interactive theorem proving via the proof assistant Lean. We study its logical foundations and its applications to computer science and mathematics. The course's goals are that the students: learn fundamental theory and techniques in interactive theorem proving; (Knowledge and understanding)learn how to use logic as a precise language for modeling systems and stating properties about them; (Applying knowledge and understanding) (Making judgements)familiarize themselves with selected areas in which proof assistants are successfully applied, such as functional programming, the semantics of programming languages, and mathematics; (Knowledge and understanding) (Applying knowledge and understanding)develop practical skills which they can apply on a larger project (as a hobby, for an MSc or PhD, or in industry); (Applying knowledge and understanding) (Learning skills)get to understand the domain well enough to start reading relevant scientific papers published at international conferences such as CPP and ITP or in the Journal of Automated Reasoning. (Applying knowledge and understanding) (Learning skills) (Communication skills)Proof assistants can be used to check the correctness of the specification of a program or the proof of a mathematical theorem. In the practical part of the course, we use the proof assistant Lean 4 to prove mathematical theorems in a precise, formal way, and see how to verify small programs. We cover the basics of interactive theorem proving, functional programming (datatypes, recursive functions), logic programming (inductive predicates), and semantics of imperative programming languages (operational and denotational; Hoare triples). We discuss some mathematical applications.2 lectures per week (90 minutes each), 2 practical sesssion per week (90 minutes each)The written exam counts for 75%, and the homework assignments count for 25% of the final grade. There will be four assignments, each corresponding to one of the major topics of the course. Assignments consist of a theoretical part and a programming part in Lean.The course notes "The Hitchhiker's Guide to Logical Verification", by Baanen, Bentkamp, Blanchette, Hölzl, and Limperg, available as a PDF on the course's web site.MSc Computer ScienceThe main prerequisites for this course are an introduction course in logic and familiarity with equational programming or functional programming (e.g., Haskell, OCaml, Scala, Standard ML).