80-211 Logic and Mathematical Inquiry

9 units, Carnegie Mellon University

How can we tell if an argument is logically sound or if it contains errors? How do we conclusively demonstrate that an argument is correct? Since ancient times, mathematical arguments have served as a paradigm of logical rigor; within mathematics, there is increasing interest in "formalizing" proofs to more firmly establish their correctness, especially proofs that are very long and complex. In the 20th century, formalization was done by writing a proof in the language of formal logic, where arguments must follow strict rules; in the 21st century, formalization is done with computer proof assistants, specialized programming languages that can check proofs and detect gaps in reasoning. In this course, we will study fundamental mathematical concepts and informal proofs as they occur in everyday mathematics, and we will use the tools of mathematical logic and the Lean proof assistant to produce fully rigorous, machine-checked formal proofs.

Prerequisites: none listed

Offered: Fall 2026

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