Primary Supervisor: Dr Christopher Birkbeck This fully funded PhD project, based at our Norwich campus, offers an opportunity to work
at the intersection of number theory, artificial intelligence and formal mathematics. You will investigate how AI can help us formalise and deepen our understanding of the Langlands program, with the aim of producing new mathematical insights, proving new results and strengthening existing ones. A concrete starting point will be the local Langlands correspondence for GL2(F) where F is a non-Archimedean local field. This correspondence provides a deep bridge between harmonic analysis and number theory, relating irreducible admissible representations of GL2(F) to two-dimensional Weil–Deligne representations. Using AI tools alongside the Lean 4 proof assistant, you will work towards formalising this correspondence, developing computer-verified definitions and theorems on both sides and progressing towards its construction and proof. You will have access to leading AI tools to support both formalisation and mathematical exploration. You will investigate how these tools can help you understand difficult arguments, work through examples, formulate conjectures, explore proof strategies and develop formally verified proofs. A central theme will be the interaction between mathematical understanding and formalisation: using the process of making definitions and arguments precise to clarify existing mathematics and motivate new research questions. The project is not limited to verifying known results. Alongside the formalisation effort, you will use AI to explore questions within the wider Langlands programme, seeking opportunities to establish new theorems and insights, extend or sharpen existing results, and find simpler or more conceptual proofs. These investigations will develop together with the formal work, with insights from each helping to guide the other. The ambition is to produce both reusable, computer-verified mathematics and original contributions to number theory, while developing effective ways to combine AI-assisted exploration with rigorous mathematical proof. Entry Requirements The minimum entry requirement is 2:1 in Mathematics. Mode of Study Full-Time Start date 1 October 2027 Additional Funding Information This four-year funded studentship, starting in October 2027, comprises tuition fees at Home fee rate, an annual tax-free stipend at the UEA rate (£20,409 in 2026/27, subject to any agreed inflationary uplift for 2027/28), and a Research Training Support Grant of £3,000 per annum. It is open to applicants eligible for Home fee status.
