| EPSRC Reference: |
EP/H023119/1 |
| Title: |
The potential of automated reasoning tools to assist the working mathematician |
| Principal Investigator: |
Bundy, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research |
| Starts: |
15 February 2010 |
Ends: |
14 February 2011 |
Value (£): |
100,616
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
20 Nov 2009
|
ICT Prioritisation Panel (Nov 09)
|
Announced
|
|
|
Summary on Grant Application Form |
|
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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ed.ac.uk |