Modular forms and formalisation (BIRKBECKC_U24SCI)

Modular forms are highly symmetric functions playing a key role in the Langlands program, helping create deep links between number theory, geometry, algebra and analysis. Creating these links have led to huge breakthroughs, such as modularity theorems, which are a key ingredient in the proof of Fermat’s Last Theorem. It is therefore unsurprising that this is one of the most active areas of research with many mathematical tools being created and studied. This makes it an attractive area of research and an excellent target for formalisation.

The area of formalised mathematics has seen huge growth, with mathematicians and computer scientists seeking to create a unified digital library of formalised mathematics results. The aim being to use. specialised computer languages, such as Lean, to code mathematical definitions, theorems and proofs. This digital format not only verifies the validity of the mathematics, but it also allows novel applications of machine learning tools (such as ChatGPT) to pure mathematics.

This project offers the opportunity to combine novel research in algebraic number theory and formalisation. One  avenue of investigation will be the study modular forms and their generalisations with a view to understanding the geometry of certain p-adic manifolds, known as eigenvarieties. For this one can construct spaces of modular forms attached to quaternion algebras, allowing for more explicit descriptions of these spaces. Alongside this, there will be the opportunity to join ongoing formalisation efforts in the area, for example by formalising quaternionic modular forms or more ambitious projects involving the formalisation of modular curves, p-divisible groups or abelian varieties.

Entry requirements

Masters is required. Acceptable first degree: Mathematics.

Start date

October 2024