Mechanized Proof

Thursday, October 13, 2016 - 13:00
427 Thackeray Hall
Speaker Information
Jacob Gross

Abstract or Additional Information

At the end of September, the problem of computer verifying the elliptic curve group laws was proposed to the group. This in mind, we will give an overview of computer aided mathematical proof. In particular, we will discuss what mechanized proof is, some tools available for doing it, how to get started learning to use these tools and the non-standard mathematical foundations one will encounter when working with a proof assistant.