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 CoInvestigators: 

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 userfriendly, 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 nonacademic 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 