This PhD project at The University of Manchester focuses on advancing the field of neural theorem proving, with a particular emphasis on formalized mathematics using the Lean interactive theorem prover. Formalized mathematics is experiencing rapid growth, with mathematicians increasingly using tools like Lean to validate and collaborate on mathematical proofs. The mathlib library, containing over 210,000 Lean proofs, exemplifies the scale and collaborative potential of this approach. However, the process of formalizing proofs remains highly labor-intensive, prompting the development of AI-based tools to automate and assist in proof generation and validation.

The project addresses two core research questions: (1) How well can current AI models actually prove mathematical theorems? (2) How can we guide and improve the proving capabilities of AI models? To answer these, the research will develop methods inspired by automated program testing and empirical analysis of proof difficulty, as well as invent fine-tuning and training procedures to enhance AI proof capabilities.

The project is supervised by Prof U Sattler, Dr D Winterer, and Dr A Mukherjee in the Department of Computer Science. Applicants should have, or expect to achieve, at least a 2.1 honours degree or a master’s (or international equivalent) in a relevant science or engineering discipline.

The position is a 3.5-year PhD, with excellent candidates nominated for competence-based competition funding. The start date is October 2026. The university values diversity and inclusion, encourages applicants from all backgrounds, and offers flexible study arrangements. Prospective students are strongly encouraged to contact the supervisors before applying, providing details of their academic background and motivation.

Applications must be submitted online, including all required documents such as transcripts, CV, supporting statement, and referee contact details. For further information or questions about the application process, applicants can contact the admissions team at [email protected].