University of East Anglia, UK
Location: Norwich
Degree: PhD
Funding: Self-funded
Study mode: Full-time or part-time
Deadline: 30 November 2026
Start date: 1 February 2027
Reference: BIRKBECKC_U27EMPSFPF
Project
This PhD will focus on formalising the local Langlands correspondence for GL₂(F) using the Lean interactive theorem prover and AI agents.
Research areas include:
• Number theory
• Representation theory
• Formal mathematics
• Lean theorem proving
• AI-assisted mathematical formalisation
• Galois representations
• Non-Archimedean local fields
The project will develop computer-verified mathematical libraries for:
• Representation theory of GL₂(F)
• Irreducible admissible representations
• Two-dimensional Galois representations
• Weil groups of local fields
The later stage of the project will develop a framework for formalising the proof of the correspondence.
Entry requirements
• Minimum 2:1 Bachelor’s degree
• Master’s degree in Mathematics
Funding
This is a self-funded PhD project.
Applicants may be self-funded or in the process of securing external funding.
A bench fee is payable in addition to tuition fees. Applicants should contact the primary supervisor for details.
UEA alumni may be eligible for a tuition fee discount.
Primary supervisor
Dr Christopher Birkbeck
Application deadline
30 November 2026