Skip to main content
Back to top
Ctrl
+
K
Automatic Theorem Proving in Mathematics
Automatic Theorem Proving in Mathematics
The six lectures
Lecture 1 — A general introduction to type theory
Lecture 2 — Simple calculations with the Church λ-calculus
Lecture 3 — Propositional logic proofs
Lecture 4 — Introduction to Lean
Lecture 5 — Advanced Lean
Lecture 6 — Auto-formalization of mathematics with Lean
The Lambda Lab cookbook
The Lambda Lab cookbook
Grand calculations
Puzzles and extended exercises
Curiosities and lore
What this lab can do
Appendix
λ-calculus quick reference
References & further reading
Index