Guiding and Evaluating Neural Theorem Proving

The University of Manchester Department of Computer Science

Prof U Sattler Dr Dominik Winterer Dr Anirbit Mukherjee

Applications accepted all year round

Competition Funded PhD Project (Students Worldwide)

About the Project

Formalized mathematics is booming [1,2,3,4].Traditionally validated manually, mathematicians increasingly formalize and validate proofs in Lean, the interactive theorem prover [5,6]. Besides automating validation, formalizing proofs as programs eases collaboration. A prime example is mathlib [7], a collection of more than 210,000 Lean proofs, which was realized in the past 8 years.

Despite such impressive efforts, formalizing proofs in Lean remains very labor-intensive. To ease this process, researchers have recently been proposing AI-based tools. With ever increasing capability, the dream is that soon, AI completes intricate proofs, beyond human capability. This raises the following fundamental research questions.

RQ1: How well can current AI models really prove?

RQ2: How can we guide AI models to improve their proving capabilities?

The Ph.D project aims to address RQ1 by inventing methods inspired by automated program testing with empirical insights on proving hardness. RQ2 will be addressed by invention of fine-tuning and training procedures to improve proof capability

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 related discipline.

This is a 3.5-year PhD is funded by the School of Engineering. Excellent candidates will be nominated for competence-based competition funding. The start date is October 2026. Excellent candidates will be nominated for competence-based competition funding. The start date is October 2026.

We strongly recommend that you contact the supervisors for this project before you apply. Please include details of your current level of study, academic background and any relevant experience and include a paragraph about your motivation to study this PhD project.

Apply online through our website: https://uom.link/pgr-apply-2425

When applying, you’ll need to specify the full name of this project, the name of your supervisor, if you already having funding or if you wish to be considered for available funding through the university, details of your previous study, and names and contact details of two referees.

Your application will not be processed without all of the required documents submitted at the time of application, and we cannot accept responsibility for late or missed deadlines. Incomplete applications will not be considered.

After you have applied you will be asked to upload the following supporting documents:

• Final Transcript and certificates of all awarded university level qualifications
• Interim Transcript of any university level qualifications in progress
• CV
• Supporting statement: A one or two page statement outlining your motivation to pursue postgraduate research and why you want to undertake postgraduate research at Manchester, any relevant research or work experience, the key findings of your previous research experience, and techniques and skills you’ve developed. (This is mandatory for all applicants and the application will be put on hold without it).
• Contact details for two referees (please make sure that the contact email you provide is an official university/work email address as we may need to verify the reference)
• English Language certificate (if applicable)

If you have any questions about making an application, please contact our admissions team by emailing FSE.doctoralacademy.admissions@manchester.ac.uk.