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.