Six lectures that build from the ground up — the λ-calculus and type theory, then propositional proofs, then Lean, and finally the auto-formalization of real research mathematics. Every idea appears twice: once as something you can run, once as something a machine checks.
The course has a single spine: a term is a proof, a type is a proposition, and a proof assistant is just a very careful accountant of that correspondence. We start where computation itself starts — a variable-binding rule you can write on a napkin — and end at a research paper checked by a kernel.
Each lecture pairs a hands-on strand (the Lambda Lab, a Lean game, a notebook) with a rigorous one (definitions, theorems, machine-checked proofs). These notes will grow as the course runs — foundations first.
What is a type, and why do modern proof assistants stand on type theory rather than set theory? We meet judgments Γ ⊢ t : A, the simply-typed λ-calculus, Church- vs Curry-style typing, and a first glimpse of dependent types — the on-ramp to everything that follows.
The untyped λ-calculus as a computational substrate: α-equivalence, capture-avoiding substitution, β/η-reduction and normal forms. Then Church encodings — booleans, numerals, the tricky predecessor, and the Y-combinator — each reduced by hand and reproduced live in the Lambda Lab.
Natural deduction and the BHK / Curry–Howard reading of the connectives (→ is a function, ∧ a product, ∨ a sum, ¬ is →⊥), taught through Emily Riehl's Lean game A Reintroduction to Proofs. Every game level maps to one inference rule.
From paper to kernel. Term mode vs tactic mode; propositions vs data; Nat, induction and rewriting; the essential tactics (intro, apply, rw, simp, induction, omega). We work through the Natural Number Game and Macbeth's Mechanics of Proof to a first honest end-to-end theorem.
Dependent types in practice: structures and typeclasses, the architecture of Mathlib and how to search it, and the heavy tactics that make formalization tractable (simp, ring, linarith, omega, norm_num, decide), calc blocks, and well-founded recursion — closing on a genuine analysis/algebra proof.
Where AI meets the kernel. The 2024–2026 landscape — AlphaProof, AlphaGeometry, DeepSeek-Prover, LeanDojo — and what "autoformalize" really means. Then the flagship case study: the EML project formalizing arXiv:2603.21852, every elementary function from a single binary operator, checked sorry-free by Lean.
In the last two years, machine-checked proof went from a niche to a frontier: AI systems reached medal territory on olympiad problems, and mathematicians began formalizing new results as they proved them. This course teaches the substrate underneath that shift.
Figures cross-checked against primary sources by the course's research pass (21 of 30 volatile claims confirmed; corrections logged in research/fact_checks.md).
The full text-friendly notes — mathematics, runnable code, and links. The "learning data" of the course, built with JupyterBook.
A full λ-calculus laboratory in your browser: step-highlighted reductions, an interactive Curry–Howard prover, type inference & inhabitation, twelve guided tutorials, quizzes, Alligator Eggs — no install.
New: a 19,000-word verified playground — Fibonacci without recursion, Ackermann in one line, a terminating Y-combinator factorial, the Ω that grows, puzzle ladders with hidden solutions. Every output produced by the real engine.
One reveal.js deck per lecture, to follow along live and revisit afterwards.
The same theorems proved in Lean, Agda, Rocq and Mizar — four foundations, one Rosetta stone.
Everything is open: book, lab, vault, artifacts, and a reproducible build. nasqret/vietnam2026.
The capstone formalization — all elementary functions from one binary operator, and its live Tree Builder demo.
