This two-week block course at Freie Universität Berlin offers a hands-on introduction to formal proof verification with the Lean theorem prover. Lectures take place at the Zuse Institute Berlin (ZIB); tutorial rooms at FU will be assigned once enrollment is known. The course is open to all (including guest auditors), with tutorial priority for FU students taking it toward ABV requirements. Please bring a laptop for in-class exercises. A solid grasp of Analysis I and Linear Algebra I is expected; no programming background is required, though technical curiosity helps. The teaching language is English (German contributions are welcome). Full details and materials—including modules on logic, set theory, natural numbers, the infinitude of primes, and basic graph theory—are available on the course GitHub.

For Master’s credit, the course adds differentiated exercises and advanced assessment. Exercises are tiered into foundational tasks (with human-readable proof templates), Master’s-level problems, and optional stretch challenges, with guidance and informal progress checks during sessions. The final assessment is a written exam that tests both conceptual understanding and practical Lean skills. In addition, Master’s students complete a Lean formalization project (individually or in pairs) and present it in an oral-exam-style session one to two weeks after the block course; M.Sc. grades are based on both the exam and the project.