The potential of automated reasoning tools to assist the working mathematician
Lead Research Organisation:
University of Edinburgh
Department Name: Sch of Informatics
Abstract
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 aim to formalize the theory of convex analysis and optimization in Isabelle, which is one of the areas of expertise of the VR. This will significantly improve Isabelle's library, since convex optimization techniques are currently one of the central techniques for addressing optimization problems in mathematics and applications, and will form the basis for further important mathematical formalisations. More importantly, we aim to provide detailed feedback to Isabelle and Proof General developers, describing what should be improved in the system to make it more attractive to mathematicians. Building on this critique, we will revise the documentation of Isabelle, and its Proof General interface, to produce versions targeted at working mathematicians.
Planned Impact
Who will benefit from this research? The beneficiaries will be users of interactive proof systems, especially Isabelle and Proof General, as discussed in the Academic Beneficiaries section. How will they benefit from this research? These tools will be improved to make them better suited to support mathematical research. In particular, there will be a new library, more targeted documentation and feedback and recommendations for further improvements. What will be done to ensure that they have the opportunity to benefit from this research? These deliverables will be developed in close consultation with both the Isabelle and Proof General developers and user communities in order to maximise their impact. Soundings will also be taken amongst a small, local community of mathematicians interested in the use of automated proof tools within mathematics. Consultation will be by both face to face and electronic communication. There will be visits to the key labs: Cambridge, Munich and Birmingham, plus a presentation at a relevant conference or workshop and a journal paper. We hope that the library and revised documentation will be circulated with the standard Isabelle release.
Organisations
Publications
Alan Bundy (Author)
(2011)
Lower Semicontinuous Functions
in Archive of Formal Proofs
Bogdan Grechuk
(2010)
Isabelle Primer for Mathematicians
Bundy A
(2011)
Automated theorem provers: a practical tool for the working mathematician?
in Annals of Mathematics and Artificial Intelligence
| Description | 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. |
| Exploitation Route | The Visiting Researcher has been appointed a lecturer in the Mathematics Department at Leicester Univeristy, where he continues to explore the application of automated provers in the development of financial mathematics, e.g., to verify correctness of the algorithms used in the finance sector. Some mathematical results formalized by Bogdan Grechuk are included in the Archive of Formal Proofs and can be used by anyone interested in formalization of mathematical proofs in Isabelle. The findings could be used in all areas of mathematics, in which automated provers can be used to assist with the proofs of the routine parts of mathematical proofs, speeding their development and ensuring a high degree of correctness. For instance, Tom Hales has recently completed the formal verification of his proof of the Kepler Conjecture, using Isabelle and HOL Light. Grechuk's findings will make such tools accessible to a wider group of mathematicians. |
| Sectors | Other |
| Description | This short project had a diverse range of impacts: 1. The VR, Dr Grechek, was appointed to a lectureship in financial mathematics in the Mathematics Department at the University of Leicester. 2. The results of the project formed the basis for a joint Edinburgh/Leicester grant proposal to the Leverhulme Trust, from the VR and two of the grant holders, entitled Making interactive theorem provers easier for mathematicians to use, with application to Financial Mathematics. At the time of writing this proposal has successfully passed the outline stage and we are awaiting the final decision. 3. A number of improvements were made to, or are under development for, automated proof systems to make them more usable by working mathematicians. For instance, the addtion of the HOL Light theorem prover to the HETS system by the HETS developers, which should provide the opportunity of translation of (at least) lemma formulation from HOL Light to Isabelle. 4. The Isabelle primer has proved popular as a, much needed, easy introduction to Isabelle for new users. |
| First Year Of Impact | 2010 |
| Sector | Digital/Communication/Information Technologies (including Software) |