80-604 Formal Methods: Human-Centered Automated Proof Search
6 units, Carnegie Mellon University
The course is designed for graduate and advanced undergraduate students in philosophy, computer science, and mathematics with deep interests in interactive theorem proving and automated proof search. The first third of the course presents a logical calculus that is, so one of its inventors claimed, "as close to mathematical reasoning as possible" (Gentzen). This natural deduction calculus is being used widely as the logical framework for the "natural formalization" of mathematical proofs, be they constructive or classical. Some important examples will be discussed. In the second third of the course the calculus itself is being investigated. With novel techniques, so-called "normal form theorems" will be established for the calculus in its constructive and classical version: Any proof can be transformed into a "normal" one. The special structural features of normal proofs will be shown. The last third of the course exploits these structural features for the interactive construction and automated search for proofs. The latter is strategically guided and produces well-structured proofs that are humanly intelligible. It is in this sense that the search procedure provides a computational model of aspects of human mathematical reasoning: The automated search is human-centered. The course's content lies in the intersection of mathematical logic, computer science, and mathematics. However, it is deeply connected to an analysis of mathematical experience and to methodological problems in the foundations of mathematics. There will be discussions and readings on these historical and philosophical issues.
Prerequisites: none listed
Offered: Spring 2026
Courseweave needs JavaScript to show sections, workloads and planning tools.