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].

This PhD project at The University of Manchester focuses on the formalization and automated proof of Boolean function conjectures using large language models (LLMs) and the Lean interactive theorem prover. Formalized mathematics is rapidly advancing, with mathematicians increasingly using tools like Lean to validate proofs and facilitate collaboration. The mathlib library, for example, now contains over 210,000 Lean proofs. However, the area of Boolean function analysis—a field with deep mathematical roots and significant potential for formalization—has been relatively overlooked. This project aims to address this gap by (a) formalizing standard results in Boolean analysis and (b) developing techniques to fine-tune LLMs for generating formal proofs of known theorems in this domain. The research will explore the intersection of formal mathematics, machine learning, and circuit complexity, with the ambition of enabling LLMs to prove or refute conjectures about Boolean functions, potentially transforming approaches to longstanding problems in circuit complexity. The ideal candidate will be passionate about formal mathematics and the mathematics underlying LLMs, with top grades in advanced theoretical computer science or mathematics courses, and experience in Boolean function analysis or circuit complexity theory. A strong background in machine learning theory and/or mathematics is highly desirable. The position is a 3.5-year PhD, with excellent candidates nominated for competitive, competence-based funding. The start date is October 2026. Applicants should have at least a 2.1 honours degree or a master’s (or international equivalent) in a relevant science or engineering discipline. The application process requires an online submission with all supporting documents, including transcripts, CV, a supporting statement, and contact details for two referees. Prospective students are strongly encouraged to contact the supervisors before applying to discuss their background and motivation. The university values diversity and supports flexible study arrangements. For further details, see the project and application links provided.