Projects
I've studied a lot of interesting mathematics over the past few years and undertaken several projects to expand my knowledge beyond the curriculum. Here's an overview of those projects.
Formalising \(8\)-Dimensional Sphere Packing in Lean
Collaborators: Christopher Birkbeck, Gareth Ma, Bhavik Mehta, Seewoo Lee, Maryna Viazovska
With special thanks to: Jeremy Avigad, Kevin Buzzard, Pietro Monticone and Utensil Song
In 2022, Maryna Viazovska was awarded the Fields Medal for her work on the Sphere Packing Problem in dimension 8 and related results, including a collaborative solution in dimension 24. Both solutions use the theory of modular forms to construct 'magic' functions that satisfy the conditions of an important intermediate result due to Cohn and Elkies. This project attempts to formalise Viazovska's solution in dimension 8 in the Lean Theorem Prover.
For my Master's project, undertaken under the supervision of Bhavik Mehta, I worked on formalising parts of Sections 4 of the original paper, which involves constructing the magic function in \(8\) dimensions and showing that it satisfies the conditions of Cohn and Elkies's result. For my work, I was awarded the Best Final-Year Individual Research Project prize and nominated by Imperial for the UK's Best Undergraduate Project competition hosted by the Institute for Mathematics and its Applications.
This project is a work in progress. For more information, please visit the project website.
Wild Automorphisms and Where to Find Them
MATH50002: Group Research Project | Imperial College London
Supervisor: Prof. Yankı Lekili
Collaborators: Jaimin Shah, Ruoceng Xu, Rongqian Ye
Polynomial rings are among the most important classes of algebras over fields \(k\), and have been studied rigorously for decades. It is surprisingly challenging to prove seemingly straightforward results about the \(k\)-automorphisms of these algebras. While all \(k\)-automorphisms are invertible by definition, it is generally quite difficult to compute an explicit inverse. Fortunately, for a large class of \(k\)-automorphisms, known as tame automorphisms, the inverse can be easily computed. Unfortunately, it is not generally known whether all \(k\)-automorphisms are tame.
By the mid-20th Century, it was known that all \(k\)-automorphisms of the polynomial rings in one and two variables are tame. However, in 1972, Nagata constructed a \(k\)-automorphism of the ring in 3 variables which he conjectured to be wild (ie, not tame). In our project, we investigated the theory developed by Shestakov and Umirbaev in 2004 to prove Nagata's conjecture when \(\operatorname{char}(k) = 0\), creating a Python library to perform the necessary symbolic computations. Our primary reference was Chapter 1 of the book Polynomial Automorphisms and the Jacobian Conjecture by van den Essen, Kuroda and Crachiola.
Simple Groups of Lie Type and Related Algorithms
Summer UROP, 2023 | Imperial College London
Supervisor: Dr. Michele Zordan
Collaborators: Linxiao Cheng
This project involved reading about topics in Commutative Algebra, Group Theory and Representation Theory to the ambitious end of being able to understand Plesken and Fabiańska's \(L_2\)-Quotient Algorithm for Finitely Presented Groups.
A Formalisation of the Existence of Partial Fraction Decompositions
Summer UROP, 2022 | Imperial College London
Supervisor: Prof. Kevin Buzzard
It is a well-known fact in commutative algebra that given an integral domain \(R\), an arbitrary polynomial \(f \in R[X] \) and pairwise coprime polynomials \(g_1, \ldots, g_n \in R[X]\), there exist \(q, r_1, \ldots, r_n \in R[X]\) such that in the field of fractions of \(R[X]\), we have the equality \[ \frac{f}{\prod_{i=1}^{n} g_n} = q + \sum_{i=1}^{n} \frac{r_i}{g_i} \] with \(\deg\!\left(r_i\right) \lt \deg\left(g_i\right)\) for all \(i\). In Summer 2022, I formalised this existence result in Lean 3. My work was subsequently merged into mathlib3, the previous version of the central Lean mathematics library, and eventually ported to mathlib4, the current version.
A Formalisation that Groups of Order \(p^2\) are Abelian
Summer UROP, 2022 | Imperial College London
Supervisor: Prof. Kevin Buzzard
Back when I first discovered the wonders of group theory, I chanced upon the fascinating—and seemingly bizarre—fact that any group of order \(p^2\) is abelian. In June 2022, I learnt the mathematics necessary to prove this result as part of the Individual Research Project I had to undertake in my first year, and over the summer, I formalised the statement and proof of this result in Lean 3. While my work was not merged into mathlib3 because another proof of this result was merged shortly before I finished, this was my first attempt at formalising previously unformalised mathematics in Lean.
Trans4m8
Computer Science Project | International Baccalaureate Diploma Programme
I developed a GUI desktop application to help the maths teachers at my school teach students how translating and scaling \(\mathbb{R} \to \mathbb{R}\) functions affects their plots. Please forgive the clunkiness: this was my very first (and so far, only) attempt at developing and distributing software.
Focus Groups
Great minds work best together!
Weekly Packathons
Carnegie Mellon University, since Fall 2025
Every Monday at 11 am Eastern Time, we have a 'packathon' (in-person at the Hoskinson Center at CMU and virtually on Zoom) where anyone interested in the sphere packing formalisation can show up, talk about their work, exchange ideas, and collaborate! If you'd like to join us, check out the Zulip thread (or send me an email)!
Sphere Packing Working Group
ItaLean Workshop, Bologna, 9-12 December 2025
In December 2025, I will lead a working group of interested formalisers at the ItaLean Workshop in Bologna to make progress on the formalisation of the 8-dimensional sphere packing problem in Lean. If you are attending the workshop and would like to join us, please get in touch with myself or Pietro Monticone.