WoLLIC 2015
Workshop on Logic, Language and Information
July 20 - 23, 2015
Indiana University, Bloomington
John Harrison: Formalization of Mathematics for Fun and Profit
Recent years have seen the completion of several very large formal proofs, including the Feit-Thompson theorem and Hales's proof of the Kepler conjecture. These show that formalization of mathematics is feasible and can perform a useful role in checking the correctness of proofs that challenge the traditional peer review process. I will be reviewing some of these achievements and addressing some common questions including:
- How reliable are these machine-checked proofs compared with informal mathematics?
- Is it realistic to expect more mathematicians to use formal proof systems?
- How can we make other uses of the large libraries of formal theorems that have been developed?
School of Informatics and Computing, Indiana University.