Skip to main content
Back to top
Ctrl
+
K
Formalized mathematics and proof assistants
Introduction
1. Type theory
2. Lean installation party
3. More type theory & Invisible mathematics
4. A first encounter with Lean 4
5. Organizational features
6. Structures and type classes
7. Setting up a formalization project
8. Inductive types
9. Meta-programming
Repository
Open issue
Index