Russell O'Connor: Machine Verification of Incompleteness of PA

Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In this talk I will present my formalization of the Goedel-Rosser Incompleteness Theorem in Coq. This required spelling out the entire proof in full detail so that the computer could verify every step. I will discuss the approach taken for this proof. I will also discuss my experiences learning to use a proof system such as Coq.