The potential of automated reasoning tools to assist the working mathematician

Synopsis: The aim of this one-year project was a case study into the use of the Isabelle proof assistant by a working mathematician, with the following three sub-goals:
- Provide a critique and recommendations on the potential of the Isabelle proof assistant and its Proof General interface for use by working mathematicians.
- Formalize the theory of convex analysis and optimization in Isabelle as a library package.
- Revise the documentation of Isabelle and Proof General to produce a version targeted at working mathematicians.
Results: The three sub-goals were achieved.
- Critique and recommendations were provided to the Isabelle developers as part of an extended exchange via the Isabelle users’ email list over the whole course of the project. Journal paper was published discussing the general use of theorem provers by working mathematicians. The Isabelle primer also included some more specific critiques of this proof assistant from the viewpoint of the working mathematician.
- The results of the formalisation were recorded in The Archive of Formal Proofs, which contains Isabelle formalisations that are assessed by the Isabelle developers as being of significant interest to other users.
- The revised documentation is collected in the primer, which is written specifically for mathematicians who are not familiar with automated provers.