Automatic Theorem Proving in Mathematics

Automatic Theorem Proving in Mathematics#

A six-lecture VIASM mini-course · Hanoi 2026

dr Bartosz Naskręcki — Faculty of Mathematics and Computer Science, Adam Mickiewicz University in Poznań · Centre for Trustworthy AI (CCAI), Warsaw University of Technology. Landing page · Lambda Lab · Source

This is the knowledge book of the course — the text-friendly notes, with the mathematics, the code, and the links in one place. It grows lecture by lecture; we build the foundations first, then climb.

The through-line#

The whole course rests on a single idea, stated four ways:

A term is a proof. A type is a proposition. Computation is proof normalization. A proof assistant is a machine that checks this correspondence without ever getting tired.

We start where computation itself starts — a variable-binding rule you can write on a napkin, the \(\lam\)-calculus — and end at a genuine research paper checked, line by line, by a kernel.

How to read this book#

Every idea appears twice:

Informally, as something you can run: a reduction in the Lambda Lab, a level in a Lean game, a small notebook.
Formally, as something a machine checks: a definition, a theorem, a proof term. The shared artifacts prove the same statements in Lean, Agda, Rocq and Mizar.

Try it now

Open the Lambda Lab in another tab and type reduce AND TRUE FALSE. It runs entirely in your browser — no install. We will use it constantly in Lecture 2.

The six lectures#

A general introduction to type theory — judgments, the simply-typed \(\lam\)-calculus, Church vs Curry, and why proof assistants stand on type theory.
Simple calculations with the Church \(\lam\)-calculus — \(\beta/\eta\)-reduction, Church booleans and numerals, the predecessor, the \(Y\)-combinator.
Propositional logic proofs — natural deduction and Curry–Howard, taught through Emily Riehl’s A Reintroduction to Proofs.
Introduction to Lean — term vs tactic mode, Nat, induction, the Natural Number Game, a first real proof.
Advanced Lean — dependent types, typeclasses, simp/ring/linarith, Mathlib, a genuine analysis/algebra proof.
Auto-formalization of mathematics with Lean — the 2024–2026 AI landscape and the EML project as a worked case study.

How to work with this course#

Each lecture has four coordinated layers. Use them in this order:

Before the lecture — skim the note (15 min). Read the Abstract, Learning objectives and Why this matters of the chapter; don’t fight the details yet.
During the lecture — follow the slides, and when a “Run it” moment appears, actually run it: keep the Lambda Lab open in a second tab. Every command in these notes is a clickable deep link that types itself into the lab.
After the lecture — work the note properly. Reproduce the worked examples by hand and in the lab, then do the exercises. Stuck? The lab’s hint (inside prove/tutorial), kb <topic>, and help <command> are there precisely for that moment.
To make it stick — one guided tutorial (in the lab: tutorial lists twelve) and a quiz bundle per lecture (quiz bundles; term answers are graded up to α-equivalence, so any correct spelling wins).

Keep the λ-calculus cheatsheet open in a third tab — one page with every definition, every encoding, and a lab command for each.

The one habit that matters

Never read a reduction — run it. The lab shows the next redex highlighted at every step, will honestly tell you when a term has no normal form, and grades your answers up to α-equivalence. The difference between reading λ-calculus and doing it is the whole course.

Note

These notes are being actively written during the course. Chapters deepen as we go, and each lecture’s current state is marked at its top.