Formalized mathematics is experiencing rapid growth, with mathematicians increasingly using interactive theorem provers like Lean to validate proofs. The Lean ecosystem, including the extensive mathlib library, has enabled collaborative formalization of over 210,000 proofs. However, the process remains labor-intensive, prompting the development of AI-based tools to automate and enhance proof validation. The dream is for AI to eventually complete intricate proofs beyond human capability. This PhD project, based at The University of Manchester's Department of Computer Science, addresses two fundamental research questions: (1) How well can current AI models really prove? (2) How can we guide AI models to improve their proving capabilities? The project will invent methods inspired by automated program testing to empirically assess proving hardness and develop fine-tuning and training procedures to enhance AI proof capabilities. Applicants should hold, 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 fully funded for 3.5 years by the School of Engineering, with excellent candidates nominated for additional competence-based competition funding. The start date is October 2026, and flexible study arrangements (including part-time options) may be considered depending on the project and funding. To apply, candidates should contact the supervisors to discuss their academic background and motivation for the project. Applications must be submitted online, specifying the project title, supervisor name, funding status, previous study details, and contact information for two referees. Required supporting documents include transcripts, CV, a supporting statement, and an English language certificate if applicable. Incomplete applications will not be considered. The University of Manchester is committed to equality, diversity, and inclusion, actively encouraging applicants from all backgrounds and career paths. The research environment is collaborative and interdisciplinary, with opportunities to engage in cutting-edge work at the intersection of artificial intelligence, software engineering, and pure mathematics. For further information, reference materials and application links are provided, including resources on Lean, mathlib, and recent advances in neural theorem proving. For application queries, contact the admissions team at [email protected].