Developing an intuitive automated theorem prover
Lead Research Organisation:
University of Cambridge
Department Name: Pure Maths and Mathematical Statistics
Abstract
Working with Prof Tim Gowers (Combinatorics) as part of the Cantab Capital Institute for the Mathematics of Information.
Proof assistants and automated reasoning tools are used sparingly by mathematicians, and usually as a last resort. This project aims to explore how these tools could be improved to make them more appealing to mathematicians. We intend to achieve this by building systems which reason in a human-like way using web technologies. The aim is that this web-app will be able explain how it arrived at a given proof, so the first applications of this are likely to be useful as a teaching aid to undergraduates.
In broad terms, I want to develop systems which help to overcome this usability problem and make automated theorem provers work better for mathematicians. To achieve my aim of developing an intuitive automated theorem prover, I will need to complete the following tasks:
1. Translation of mathematical knowledge to an easily computable form. This can be achieved either through manual entry or linguistic analysis of existing texts as demonstrated in [2].
2. Synthesis of natural language proofs from existing formal proofs.
3. Developing logics and heuristics for proving theorems in a way that mimics how a human would prove theorems.
4. Creating user interfaces which allow a non-specialist user to intuitively operate the given system.
I am interested in all of the above problems, but the scope is too large to be undertaken as a PhD project. In terms of producing theoretical results, I will mainly concern myself with (3). But I will also be implementing existing research on (1) and (2) as well as producing user interfaces.
Proof assistants and automated reasoning tools are used sparingly by mathematicians, and usually as a last resort. This project aims to explore how these tools could be improved to make them more appealing to mathematicians. We intend to achieve this by building systems which reason in a human-like way using web technologies. The aim is that this web-app will be able explain how it arrived at a given proof, so the first applications of this are likely to be useful as a teaching aid to undergraduates.
In broad terms, I want to develop systems which help to overcome this usability problem and make automated theorem provers work better for mathematicians. To achieve my aim of developing an intuitive automated theorem prover, I will need to complete the following tasks:
1. Translation of mathematical knowledge to an easily computable form. This can be achieved either through manual entry or linguistic analysis of existing texts as demonstrated in [2].
2. Synthesis of natural language proofs from existing formal proofs.
3. Developing logics and heuristics for proving theorems in a way that mimics how a human would prove theorems.
4. Creating user interfaces which allow a non-specialist user to intuitively operate the given system.
I am interested in all of the above problems, but the scope is too large to be undertaken as a PhD project. In terms of producing theoretical results, I will mainly concern myself with (3). But I will also be implementing existing research on (1) and (2) as well as producing user interfaces.
Organisations
People |
ORCID iD |
| W Gowers (Primary Supervisor) | |
| Edward Ayers (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509620/1 | 01/10/2016 | 30/09/2022 | |||
| 1804138 | Studentship | EP/N509620/1 | 01/10/2016 | 31/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 |