Lean is an open-source functional programming language
that allows formalising mathematical definitions and proofs.
It can also prove easy goals automatically and
fill in routine steps.
By the end of the course, students should be able to:
1. read and navigate simple Lean files;
2. write basic tactic proofs;
3. locate and use existing lemmas from mathlib;
4. formalize standard arguments from elementary real analysis;
5. complete a small collaborative or individual formalization project in analysis.
In this course we focus on topics from real analysis, especially sequences, limits, continuity, metric and topological ideas, differentiation, and introductory measure/integration.
Recommended materials:
Mathematics in Lean, especially the chapters on logic, sets and functions, topology, differential calculus, and integration/measure theory.
Tao’s Lean Analysis I companion, especially for its foundational, exercise-driven treatment of basic analysis and proof structure.
Language: English or German (depending on the participants) |
