Introduction to Formal Verification of Mathematics
MATH 161
Subject & Catalog Number
Course Information
Description
How can a computer check if a mathematical proof is completely and truly correct? This course will be an introduction into the world of formal verification of mathematics, starting with basic examples of sets and natural numbers, and moving on to more advanced mathematics. We will work with Lean, an open-source programming language for formal verification that has been used to verify large portions of mathematics, including a few examples reaching all the way to the forefront of current mathematics research.
School
Faculty of Arts & Sciences
Credits
4
Cross Reg
Available for Harvard Cross Registration
Department
Mathematics
Course Component
Lecture
General Education
N/A
Quantitative Reasoning with Data
N/A
Divisional Distribution
Science & Engineering & Applied Science
Course Level
For Undergraduate and Graduate Students
