Machine checking of mathematical proofs for undergraduate education at MIT

Mathematical proofs are a core concept in many areas of computer science and other fields, but how to write them is not especially easy to learn. The rules of the game, determining which proof steps are convincing and which are cop-outs, can seem mysterious. In the computer theorem proving world, there are some venerable algorithmic definitions of proof validity, but they have rarely been applied in contexts with non-expert proof authors. The UROP opportunity I'm proposing would join existing work to build tools for insertion of machine-checked theorem proving in undergraduate courses, such as 6.042 and others for which it is a prerequisite. Specifically, students would get instant feedback on which proof steps are correct, instead of needing to wait days for critiques by graders or other course staff. At the same time, students would learn about some tools that may form the foundation for future high-assurance software engineering, where programs come with proofs of good behavior. Possible project focuses include building a friendly Web interface for interactive proof construction; or building sample homework assignments for the class, which would include deciding on sets of allowable proof steps and implementing them in the Coq theorem proving system.

Interested candidates may contact Adam Chilipala, adamc@csail.mit.edu.