Mechanized Proof

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.