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

Building Peano Lab

Building Peano Lab
Why Peano arithmetic?
The kernel and the De Bruijn criterion
Native PA language reference
PA axioms, induction, and proof rules
Anatomy of a tactic
When tactics become a language
Induction and the checked theorem ladder
Checked arithmetic automation: compute, then certify
compact_arith: searching for a small PA certificate
Limits: what checking can—and cannot—tell us
Training a Peano policy without trusting it
Peano Hydra: where symbolic search should end and learned search begin
Checked tutorials: commands, not transcripts
The checked theorem ladder
Implementation diary

Foundational arithmetic library

The foundational arithmetic library
Alpha and Stable library editions
A guided route from zero to FTA
The Stable theorem atlas
The Alpha QR proof explorer
The definition-aware proof explorer
Curating the next conservative edition
The theorem dependency graph
Language, notation, and trust
Self-contained proof sharing
The dependency ladder
Divisibility and subtraction-free congruence
GCD and balanced Bézout construction
The strict-HA number-theory campaign
K3B Alpha: cell histories and extensional lookup
K3C Alpha: valid lists, membership, and semantic lookup
Primes and unique factorization
The quadratic-reciprocity campaign
Bertrand’s postulate campaign
The complete Bertrand proof explorer
The definition-aware Bertrand proof explorer
Sources and clean-room provenance
Using and extending the library

Appendix

λ-calculus quick reference
References & further reading

Index

By Bartosz Naskręcki

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

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