The potential of automated reasoning tools to assist the working mathematician
Most of the recently proved important mathematical theorems have proofs of several hundreds of pages and cannot be reliably verified by referees. In this context, developing a user-friendly, formal, proof assistant, where everyone can check a proof of his result, becomes vital for the future of mathematics. There exist several proof assistants, such as Isabelle, HOL, Coq, etc., but they are currently unattractive for working mathematicians. As a result, libraries of formalized mathematical results are not sufficiently rich to formalize most serious mathematical results, and, more importantly, developers of these proof assistants do not have sufficient feedback from mathematicians.
In this project we:
- formalize a part of convex analysis in Isabelle.
- provide a detailed feedback to Isabelle developers, describing what should be improved in the system to make it more attractive to mathematicians.
- write a quick introduction to the Isabelle/HOL proof assistant aimed at mathematicians who would like to start use it for the formalisation of mathematical results.
1) Formalization of convex analysis in Isabelle
We formalised a part of convex analysis in Isabelle, with the focus mostly on topological properties of convex sets. In the process, we needed to formalise significant parts of theories from other areas of mathematics. For example, we formalised notions of affine dimension and infinite reals in Isabelle. All these concepts and results are very important and basic in mathematics, so they significantly enrich the Isabelle library and hopefully will be widely used in future formalisation projects.
2) Critique of Isabelle and recommendation for improvements
We provide Isabelle developers with a broad range of concrete critiques and suggestions, which are most critical to make Isabelle more attractive for mathematical community. Clearly, some suggestions were not new to the Isabelle group, but led to extensive discussion and hopefully now their implementation will be prioritised accelerated. Some suggestion, however, were new to them. For example, the suggested "proof by analogy" tactic would significantly simplify the proving of mathematical results in Isabelle using analogical arguments (which are very popular in mathematics).
Also, we suggested to add the HOL Light theorem prover to the Hets system, which should provide us with a opportunity of translation of (at least) lemma formulation from HOL Light to Isabelle. This project has already started (in October 2010).
3) Isabelle Primer for Mathematicians
Currently, the Isabelle/HOL proof assistant attracts little attention from the mathematical community. One of the reason for this is that the Isabelle documentation is not oriented for mathematicians, and it is hard to get started We wrote the "Isabelle Primer for Mathematicians"
- a quick introduction to the Isabelle/HOL proof assistant aimed at mathematicians who would like to start use it for the formalisation of mathematical results. We have discussed only a tiny portion of Isabelle here, but it is enough to start the formalisation of some simple mathematical results. We have tried to concentrate on topics which are especially useful for a beginner: main notations, search in Isabelle, organization of blocks inside the proof, etc. More importantly, we have tried not just tell mathematicians "how it works", but to tell them how to learn Isabelle by looking at the existing theories. Instead of providing the user with correct proofs immediately, we often start with intuitive, but incorrect versions, and describe how to correct the resulting errors. This approach anticipates and heads off the kind of typical errors we expect beginning users to make.
Bogdan Grechuk, Alan Bundy
, Lucas Dixon
, David Aspinall
This research was supported by EPSRC Grant EP/H023119/1. The full proposal is available here