PhD Studentship: Formalising the Local Langlands Correspondence for GL₂(F) in Lean

Overview

This PhD project at the University of East Anglia, based at the Norwich campus and supervised by Dr. Christopher Birkbeck, sits at the meeting point of number theory, representation theory and formal mathematics. The single research aim is to begin formalising the local Langlands correspondence for GL2(F) in the Lean interactive theorem prover, using AI agents. The correspondence is a cornerstone of the modern Langlands programme, linking harmonic analysis and number theory.

The first goal is to formalise the mathematical objects needed to state the main theorem. That means building a computer-verified library for both sides of the correspondence: the representation theory of GL2(F), where F is a non-Archimedean local field, including irreducible admissible representations, and the structure of two-dimensional Galois representations of the Weil group of F. Once the definitions are in place, the second phase is to create a framework to guide formalisation of the proof itself, laying groundwork for a long-term verification effort.

Requirements

The minimum entry requirements are a 2:1 Bachelor's degree and a Master's degree in mathematics.

What you get

The project is offered on a self-funded basis, open to applicants who are self-funded or are securing external funding. A bench fee is payable in addition to the tuition fee, and details are available from the primary supervisor. UEA alumni may be eligible for a tuition fee discount.

Key dates

Study can be full or part time, starting on 1 February 2027. The closing date is 30 November 2026.