21-321 Interactive Theorem Proving

9 units, Carnegie Mellon University

Computational proof assistants now make it possible to work interactively to write mechanically verified definitions, theorems, and proofs. Important theorems have been formalized in this way, and digital libraries are being developed collaboratively by the mathematical community. Formalization of mathematics also serves as a gateway to the use of new technologies for discovery, such as automated reasoning and machine learning. This course will teach you how to formalize mathematics so that you, too, can contribute to the effort. We will explore a logical framework, dependent type theory, which serves as a practical foundation in a number of proof assistants. Finally, as time allows, we will explore ways of automating various aspects of mathematical reasoning. (Three 50 minute lectures)

Prerequisites: 15-151 or 21-127 or 21-128

Offered: Fall 2026

Courseweave needs JavaScript to show sections, workloads and planning tools.