Formalising the Local Langlands Correspondence for GL₂(F) in Lean (BIRKBECKC_U27EMPSF)

About the Project

Primary Supervisor: Dr. Christopher Birkbeck

This 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 GL₂(F) in the Lean interactive theorem prover by leveraging AI agents. 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 GL₂(F), where F is a non-Archimedean local field, including the theory of irreducible admissible representations; and (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 minimum entry requirements are a 2:1 Bachelor's degree and a Master's in mathematics.

Mode of Study

Full or Part time

Start Date

1 October 2026