European Molecular Biology Laboratory (Heidelberg) Featured PhD Programmes
Engineering and Physical Sciences Research Council Featured PhD Programmes
Birkbeck, University of London Featured PhD Programmes
Sheffield Hallam University Featured PhD Programmes
Kingston University Featured PhD Programmes

Artificial Intelligence methods for automated theorem proving


Project Description

In recent decades, the number of mathematical papers increased significantly. Tens thousands of papers are submitted to online repository arxiv each year. The proofs of some theorems in these papers are hundreds pages long. It is becoming increasingly difficult to verify the proofs of all theorems. Moreover, it is difficult even to search for mathematical results and understand whether a lemma arising in your research is new. Many mathematical results are discovered and then rediscovered multiple times by independent teams of researchers.

The idea that mathematical theorems and proofs should be verified automatically by a computer has been around for at least 45 years. In 1973, Andrzey Trybulec invented Mizar proof assistant, which is able to understand mathematical theorems and proofs typed in the specially designed Mizar formal language. There are other proof assistants like Coq, HOL Light, Isabelle, etc., with their own libraries of formally verified mathematical results. However, these proof assistants requires typing proofs in some special language, and, as a result, only a tiny fraction of mathematicians use them.

Explosive developments in Artificial Intelligence over last 10 years drastically increased modern computers’ abilities to automate and process natural language. AI algorithms are now approaching a near-human performance when translating general ordinary texts to other languages.

This project aims to make the next step forward: to develop a theorem prover with fully natural language interface. It should be able to read mathematical proofs as they are in research papers and textbooks, understand and verify them, possibly after asking some clarifying questions. The program will be AI-powered, learn continuously from human experts, and the number of such clarifying questions will soon decrease from extremely high to minimal possible level. Equipping AIs with capabilities to “learn-on-the-job” without deep re-training has been the focus of the group’s preliminary work over last 5 years.

We envision that, as a result of successful completion of this challenging project, mathematicians will be able to type their proofs as they are doing now in LaTex, with the difference that not only syntax but actual correctness of the proofs will be automatically verified leading to enormous public and scientific benefits.

Entry requirements

UK Bachelor Degree with at least 2:1 in a relevant subject or overseas equivalent.

English language requirements may apply https://le.ac.uk/study/research-degrees/entry-reqs/eng-lang-reqs/ielts-60

Enquiries

Project Specific :

Application Specific :

How to apply

To apply refer to: https://le.ac.uk/study/research-degrees/funded-opportunities/epsrc-studentships

Eligibility:
UK/EU (Residency Requirements for EU in accordance with UKRI)
https://epsrc.ukri.org/skills/students/guidance-on-epsrc-studentships/eligibility/

Funding Notes

3.5 Year funding:
Fees
RCUK Rate Stipend
RTSG
*Competitive Funding*

References

Hales, Thomas C. "Formal proof." Notices of the AMS 55.11 (2008): 1370- 1380.

Gonthier, Georges. "Formal proof–the four-color theorem." Notices of the AMS 55.11 (2008): 1382-1393.

Hales, Thomas, et al. "A formal proof of the Kepler conjecture." Forum of Mathematics, Pi. Vol. 5. Cambridge University Press, 2017.

Ganesalingam, Mohan. The language of mathematics. Diss. University of Cambridge, 2010.

I. Tyukin, A.N. Gorban, S. Green, D. Prokhorov. Fast Construction of Correcting Ensembles for Legacy Artificial Intelligence Systems: Algorithms and a Case Study, Information Sciences, 485, 230-247, 2019.

A.N. Gorban, A. Golubkov, B. Grechuk, E.M. Mirkes, I.Y. Tyukin. Correction of AI systems by linear discriminants: Probabilistic foundations. Information Sciences, 466, 303-322, 2018.

Email Now

Insert previous message below for editing? 
You haven’t included a message. Providing a specific message means universities will take your enquiry more seriously and helps them provide the information you need.
Why not add a message here
* required field
Send a copy to me for my own records.

Your enquiry has been emailed successfully





FindAPhD. Copyright 2005-2020
All rights reserved.