Skip to main content

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

Search

Ctrl+K

By Bartosz Naskręcki

© Copyright 2026 Bartosz Naskręcki — co-developed with Claude.

VIASM mini-course · Hanoi 2026 · landing page · Lambda Lab · source