PhD Studentship: Formalising the Local Langlands Correspondence for GL₂(F) in Lean
The School of Engineering, Mathematics and Physics at the University of East Anglia (UEA) invites applications for a unique PhD Studentship titled “Formalising the Local Langlands Correspondence for GL₂(F) in Lean.” Primary supervision will be provided by Dr. Christopher Birkbeck.
Project Overview: Based at the UEA Norwich campus, this PhD project offers an exceptional opportunity to conduct research at the confluence of number theory, representation theory, and formal mathematics. The successful candidate will undertake an ambitious research project focused on initiating the formalisation of the local Langlands correspondence for GL₂(F) within the Lean interactive theorem prover, leveraging AI agents to assist in the formalisation process. The local Langlands correspondence represents a central pillar of the modern Langlands program, establishing a deep and profound connection between harmonic analysis and number theory.
Programme & Mode of Study:
• Mode of Study: Available for full-time or part-time study.
• Target Start Date: February 1, 2027.
• Additional Perks: Graduates from the UEA alumni community may be eligible for a postgraduate tuition fee discount.
Eligibility Criteria:
• Minimum academic entry requirements: A 2:1 Bachelor’s degree and a Master’s degree in Mathematics or equivalent international qualifications.
• Funding Status: Offered on a self-funded basis. Open to applicants who are self-funded or who are in the process of securing external funding.
Required expertise/skills:
• Strong academic foundation in number theory, representation theory, or abstract algebra.
• Interest or background in formal mathematics, interactive theorem provers (specifically Lean), or mathematical formalisation techniques.
• Capability or interest in utilizing AI agents and computational tools within mathematical workflows.
Salary details: Not Specified / Self-Funded A bench fee is payable in addition to standard tuition fees to cover specialist equipment and laboratory facilities required for the research. Applicants should contact the primary supervisor for details regarding the applicable bench fee.
Application Deadline: November 30, 2026