Verified Computation and Proof

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Mathematics is exceedingly complex, and avoiding mistakes is crucial to keeping our mathematics correct, meaningful, and reliable. This project involves the use of logic-based computational methods to support mathematical reasoning. The PI will contribute to the development of a theorem prover called Lean, which can be used to verify complex proofs and calculations. The system enables us to build mathematical libraries that are verified on the basis of a formal axiomatic system, with the computer checking each and every claim on the basis of a small set of axioms and rules. The system will support exploration and the discovery of new mathematics, and can also be used to verify properties of complex systems in computer science, engineering, and finance. The development of Lean is based at Microsoft Research, Redmond, but it is an open-source, community-based project that currently involves researchers at Carnegie Mellon University, Stanford, and the University of Washington as well. The PI will develop Lean's libraries and automation to support applications in fields such as engineering and mathematical finance. Specifically, the PI and his collaborators and students at Carnegie Mellon will extend the libraries for analysis and measure theory and measure-theoretic probability, as well as parts of algebra and homotopy type theory. They will also contribute to other types of automation currently under development in Lean, and develop decision procedures and algorithms for special domains. Finally, they will continue to develop interactive online course material, based on Lean, to provide better educational resources for logic and formal methods.