07-31-2026, 08:17 PM
An Introduction to Automatic Theorem Proving in Mathematics
Summary
The VIASM Mini-Course 2026: “An Introduction to Automatic Theorem Proving in Mathematics” by Dr. Bartosz Naskręcki is a six-lecture course held in Hanoi that introduces the foundations and applications of computer-assisted mathematical proofs.
The course begins with type theory and the Church λ-calculus, then develops concepts from propositional logic and the Curry–Howard correspondence before moving to the proof assistant Lean, where students learn how formal proofs are created and verified by computers. Advanced topics include dependent types, Mathlib, automated tactics, and the emerging field of AI-assisted formalization of mathematics. The final lecture explores how artificial intelligence systems such as AlphaProof and other theorem-proving models are changing mathematical research by combining human ideas, AI methods, and machine-checked verification.
The course provides theoretical notes, interactive laboratories, programming exercises, and formal proof artifacts, offering a modern introduction to the intersection of mathematics, logic, programming, and artificial intelligence.
COURSE
Summary
The VIASM Mini-Course 2026: “An Introduction to Automatic Theorem Proving in Mathematics” by Dr. Bartosz Naskręcki is a six-lecture course held in Hanoi that introduces the foundations and applications of computer-assisted mathematical proofs.
The course begins with type theory and the Church λ-calculus, then develops concepts from propositional logic and the Curry–Howard correspondence before moving to the proof assistant Lean, where students learn how formal proofs are created and verified by computers. Advanced topics include dependent types, Mathlib, automated tactics, and the emerging field of AI-assisted formalization of mathematics. The final lecture explores how artificial intelligence systems such as AlphaProof and other theorem-proving models are changing mathematical research by combining human ideas, AI methods, and machine-checked verification.
The course provides theoretical notes, interactive laboratories, programming exercises, and formal proof artifacts, offering a modern introduction to the intersection of mathematics, logic, programming, and artificial intelligence.
COURSE
┌────────────────────────────────┐
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘