PhD Studentship: Formalising the Local Langlands Correspondence for GL₂(F) in Lean
University of East Anglia, UKLocation: NorwichDegree: PhDFunding: Self-fundedStudy mode: Full-time or part-timeDeadline: 30 November 2026Start date: 1 February 2027Reference: 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• … Read more