Introduction

We are two  mathematicians with an interest in computer algebra and proofs. A couple of years ago, after the announcement of the verification of the Feit-Thompson theorem, we started to dabble in the dark arts of computer proof assistants with a view towards using them in teaching. After various attempts with Isabelle and Coq we realised that, despite the fact that they seem to be very powerful and useful,  the average student will not invest enough time in learning these. With this realisation came the decision to write our own interface.

Enter  SpatchCoq! SpatchCoq is a GUI to the powerful proof assistant Coq. It lets students write structured proofs in “natural English” which are then passed on to Coq for verification on correctness and Coq provides feedback. Completed proofs can be exported to the typesetting system LaTeX.

Motivation

While proof assistants were originally developed for mathematical proofs, in reality they have mainly been used in software verification and theoretical computer science. Recently, some very important theorems in Pure Mathematics (the Four Colour Theorem, The Feit -Thompson Theorem and the Flyspeck project) have been verified with proof assistants. Current versions of proof assistants are on the brink of going beyond implementing and verifying proofs that are already known to the user. Some are able to make context driven suggestions on how to proceed with an unfinished proof and which known results to try. This means that proof assistants are getting increasingly powerful and ought to be considered as fully operational tools in conducting mathematical research, complementing the already fully established computing software such as Sage and GAP, Magma, Geogebra, Maple, Matlab, and R and many others.

Moreover, the most recent versions of certain proof assistants are becoming increasingly user friendly. For instance, Coq and Isabelle allow the user to systematically and strategically build proofs. This suggests that the area is now mature enough to be presented to mathematics students at the undergraduate and graduate level. Thus proof assistants can be introduced into the repertoire of future mathematicians and teachers. In view of the previous remarks, this is not just a possibility, but may well prove to be a necessity in building a successful mathematical career.

At the lowest level, exposure to proof assistants would offer mathematics students an access point to modern functional programming languages such as OCAML and Haskell improving their employability. At a higher level, mathematics graduates will be able to use proof assistants in their own research.

Unfortunately, at this point the available literature is aimed at computer scientists with backgrounds in functional programming and, as such, is not accessible to less computer sophisticated mathematics students.

The current project creates aids to overcome this disconnect and help open up the exciting capabilities of proof assistants to the mathematical world at large. Among other initiatives, it will produce accessible course materials aimed at integrating proof assistants into the already existing mathematical curriculum.

Downloads and feedback blog

As we are developing the GUI we will make it available here. We would like to invite anyone who so wishes to try it out and give us their feedback.