CMU 15-815 Interactive Theorem Proving

Grading and Policies

This is a graduate-level seminar. If you are taking it for credit, you are expected to keep up with the lectures, work though the exercises in the tutorial, and experiment with Lean on your own. You will also need to complete a final project, which will ideally consist of a formalization in Lean. Please consult with the instructors while choosing a topic.