Formalizing and Testing Function Boolean Conjectures with LLMs

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.

A very fruitful and concrete subject that has been overlooked by much of these recent formalization efforts is that of Boolean function analysis [8]. Because of the finite nature of such functions, we anticipate these to have a high potential of being formalizable, while at the same time Fourier analysis on the Boolean hypercube is an exceptionally deep area of mathematics. This project aims to leverage this best-of-both-worlds scenario.

The Ph.D. project aims at (a) formalizing standard results in Boolean analysis and (b) inventing techniques to efficiently fine-tune LLMs to generate formal proofs of known theorems in Boolean analysis. This Ph.D. project is very challenging. It has a far-reaching ambition of paving a new path to proving or refuting conjectures about Boolean functions with LLMs and thus bring about a paradigm shift in how we approach traditional puzzles in circuit complexity.

Ideal project outcomes include new mathematics and new mechanized formal mathematics. The ideal student is someone who is passionate about studying formal mathematics and about understanding the mathematics of LLMs. It is required that the student has top grades in advanced courses in theoretical CS or mathematics and has either done courses in or has research background in Boolean function analysis or circuit complexity theory.

Eligibility

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.

A strong background in either Machine Learning theory and/or mathematics is highly desirable.

Funding

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

Before you apply

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.

How to apply

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.