Section 2 Course Information
Subsection 2.1 Course Description
This course provides a hands-on introduction to formal verification and computer-assisted proof development using the Lean theorem prover. You will learn how to represent mathematical concepts in a precise formal language, construct and verify proofs interactively, and leverage automated techniques to eliminate logical errors. Along the way, you’ll explore core ideas from logic, type theory, and proof strategies that can be applied to create robust formalizations of everything from classical theorems to complex software specifications.
Subsection 2.2 Course Prerequisites
A grade of C or better in MATH 307, MATH 311, or CSC 220.
Subsection 2.3 Student Learning Outcomes
Mathematics students will see how formalizing arguments in Lean can reveal hidden assumptions, refine logical thinking, and spark fresh insights, even for well–known theorems. Lean also serves as a platform for cutting–edge mathematical research, with extensive libraries of verified results that encourage meaningful contributions.
Computer Science students will discover how Lean’s type–theoretic foundations apply to verifying algorithms, cryptographic protocols, and large–scale software systems, reinforcing a correctness–first mindset essential to modern development.
By the end of the course, you will be prepared to produce fully machine–checked proofs, apply formal methods to real–world challenges, and collaborate effectively with mathematicians and software engineers alike, bridging the gap between theoretical vision and practical reliability.
Subsection 2.4 Course Topics
This course provides an introduction to formal verification and computer-assisted proof development using Lean. Students will explore the following topics
-
Understanding Mathematical Statements: Learning how to write and check logical statements and rules in Lean.
-
Building Proofs Step by Step: Using tools and techniques to create clear and logical arguments.
-
Defining and Working with Data: Exploring how to represent data like numbers, lists, and trees in Lean.
-
Writing and Reasoning About Programs: Understanding how to write small programs and prove they work correctly.
-
Handling Complex Computations with Monads: Simplifying advanced programming tasks using special tools in Lean.
-
Checking Algorithms: Ensuring common algorithms, like sorting, are correct and reliable through formal proofs.
-
Foundations of Logic and Mathematics: Exploring the deeper structure of logic, types, and mathematical rules.
Subsection 2.5 Instructional Methods
This course is offered as a face-to-face course. Learning will be facilitated through traditional lecture, group work/activities, homework, and in-class assessments.
