Formalising the Local Langlands Correspondence for GL₂(F) in Lean (BIRKBECKC_U26EMP)
Key Details
- Application deadline
- 31 January 2026 for International, 31 March 2026 for Home
- Location
- UEA
- Funding type
- Self-funded
- Start date
- 1 June 2026
- Mode of study
- Full-time
- Programme type
- PhD
)
Welcome to Norwich
According to the Sunday Times, this city is one of the best places to live in the UK.
Project description
Primary supervisor - Dr Christopher Birkbeck
This self-funded PhD project, based at our Norwich campus, offers a unique opportunity to work at the confluence of number theory, representation theory, and formal mathematics. You will undertake a single, ambitious research project: to begin the formalisation of the local Langlands correspondence for GL2(F) in the Lean interactive theorem prover. This correspondence is a cornerstone of the modern Langlands program, providing a deep and unforeseen bridge between harmonic analysis and number theory.
The primary goal of this project is to formalise the sophisticated mathematical objects required to state the main theorem. This will involve developing a computer-verified library for the two sides of the correspondence:
1. The representation theory of GL2(F), where F is a non-Archimedean local field, including the theory of irreducible admissible representations.
2. The intricate structure of two-dimensional Galois representations of the Weil group of F.
Once the definitions are in place, the second phase of the project will be to create a comprehensive framework to guide the formalisation of the proof itself, laying the groundwork for a long-term verification effort. This foundational work will be a landmark achievement in the digital formalisation of contemporary mathematics.
Entry requirements
The standard minimum entry requirement is 2:1 in Mathematics.
Funding
This project is offered on a self-funding basis. It is open to applicants with funding or those applying to funding sources. Details of tuition fees can be found here.
A bench fee is also payable in addition to the tuition fee to cover specialist equipment or laboratory costs required for the research. Applicants should contact the primary supervisor for further information about the fee associated with the project.
UEA Alumni 10% Scholarships - A scholarship of a 10% fee reduction is available to UEA Alumni looking to return for postgraduate study at UEA, Terms and conditions apply. For a postgraduate master’s loan, visit our Postgraduate Student Loans page for more information.