Developing an intuitive automated theorem prover

Lead Research Organisation: UNIVERSITY OF CAMBRIDGE
Department Name: Pure Maths and Mathematical Statistics

Abstract

Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509620/1 30/09/2016 29/09/2022
1804138 Studentship EP/N509620/1 30/09/2016 30/03/2020 Edward Ayers
 
Description I have developed a series of tools to assist making formalised mathematics easier to use for a human.
The first of these is a browser based interactive prover, humanproof. The purpose of this is to explore the challenges of bringing interactive theorem proving to the domain of the browser.
The second of these is arxiv-search, a tool for searching the arxiv using elastic search.
The third is lean-subtasks, an experimental piece of proof automation technology implemented within the Lean theorem prover that aims to solve simple equality problems in a human-like way rather than through brute-force search.

In addition to these I have collaborated with the Naproche/SAD project which aims to build an interactive proof assistant in natural language as one might find in a mathematics textbook. I am also a code contributor to Lean 3, an open source theorem prover.
Exploitation Route My work primarily focusses on making automated theorem provers easier to use for non-specialists. I hope that other researchers will take my work forward in several levels of abstraction:
- Once the source code is released, others might build on my work to build better, web-native tools for theorem proving.
- Others will use my developed provers to generate more readable proofs within existing proof assistants.
- Others will use my work as evidence that proofs generated automatically do not have to be difficult for humans to read.

There are many potential real-world applications of making automated theorem provers more accessible:
- Within mathematical research: researchers will find it easier to formalise their work, massively reducing the probability of errors.
- Within higher-education: more human-oriented theorem provers will be easier to use for undergraduates. Such systems could be used to reduce the burden of marking proofs (since a formalised proof may be checked by a computer).
- Within high-complexity, low-fault-tolerance industry. Currently, computer code is full of bugs -- mistakes in coding which cause unexpected behaviour. In most applications it is sufficient to fix these bugs when they are detected. But in some industries such as aerospace, cybersecurity and computer hardware, the cost of an undetected bug can be very large. Automated theorem proving helps avoid bugs by proving that a program's bahaviour matches its specification. However such tools are tedious to use currently and so more accessible theorem provers will help in building provably correct computer programs.
Sectors Aerospace

Defence and Marine

Digital/Communication/Information Technologies (including Software)

Education

Electronics

Energy
 
Title arxiv-search 
Description This was a project to partially rewrite and extend arxiv sanity by Andrej Karpathy to all of the arXiv and add features such as Faceted search UI improvements, e.g. infinite scroll Elasticsearch as a backend database 
Type Of Technology Webtool/Application 
Year Produced 2018 
Open Source License? Yes  
Impact Ultimately, we decided to end the project due to time constraints and improvements in the native arxiv interface (see https://ericphanson.com/blog/2018/arxiv-search/). 
URL https://github.com/ericphanson/arxiv-search