Interactive Theorem Proving

9 units · Undergraduate

Fall: 9 units 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: 21-127 or 21-128 or 15-151 Course Website: https://www.cmu.edu/math/undergrad/math-course-information.html