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.
A Lean Formalisation of Sections 4 and 5 of Viazovska's Solution to the Sphere Packing Problem in \(\mathbb{R}^8\)
Master's Project, 2024-2025 | Imperial College London
Supervisor: Dr. Bhavik Mehta
With special thanks to: Prof. Maryna Viazovska, Prof. Kevin Buzzard, Utensil Song, Gareth Ma, Seewoo Lee, Dr. Christopher Birkbeck
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 for which a near-complete transformation exists in the Lean Theorem Prover. For my MSci project, I am attempting to formalise Sections 4 and 5 of her solution in dimension 8, which involve constructing the magic function in \(8\) dimensions and showing that it satisfies the conditions of the intermediate result.
This project is a work in progress, and I am committing to a private repository which also contains formalisations of dependencies that have been worked on by myself and others (including that of the aforementioned intermediate result). The official announcement was made by Professor Viazovska in a talk she gave at an ICMS workshop on the formalisation of mathematics for women and mathematicians of minority gender. The proof path follows a blueprint that was originally written by Professor Viazovska and is being edited by the people involved in this project as it progresses. The blueprint also includes a dependency graph, which will be updated as the formalisation progresses.
A Formalisation of the Cohn-Elkies Linear Programming Bounds in Lean
Summer Internship, 2024 | École Polytechnique Fédérale de Lausanne
Supervisor: Prof. Maryna Viazovska
Collaborators: Utensil Song, Gareth Ma, Seewoo Lee, Dr. Christopher Birkbeck
Maryna Viazovska's celebrated solution to Sphere Packing Problem in dimensions 8 and the collaborative solution it inspired in dimension 24 depend strongly on an intermediate result proven by Henry Cohn and Noam Elkies that gives an upper-bound on the optimal sphere packing density in \(\mathbb{R}^d\) in terms of a certain specific type of function, if such a function exists. The solutions involve constructing functions that satisfy these conditions and whose Cohn-Elkies bounds are the sphere packing densities of the \(E_8\) and Leech lattices in \(\mathbb{R}^8\) and \(\mathbb{R}^{24}\) respectively.
I had the incredible opportunity to spend the summer of 2024 in Lausanne, working with Professor Viazovska and other collaborators from across the globe on formalising the Cohn-Elkies bounds in the Lean Theorem Prover. Given that sphere packings had never been defined previously in Lean, the project involved developing a lot of theory before formalising the actual statement and proof of the Cohn-Elkies bounds. The formalisation is nearly complete, with the few remaining gaps being worked on by members of the Lean community. Our work has laid the foundations for the solutions in dimensions 8 and 24 to be formalised in Lean.
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.
Obtaining the Optimum Angle of Rotation for Regular Polygons to Maximise the Volume of the Solid of Revolution
Extended Essay | International Baccalaureate Diploma Programme
This dissertation I wrote to obtain my secondary school diploma contained a formulated and solved an geometric optimisation problem. Using little more than secondary school-level mathematics and the computational power of Wolfram Mathematica, I determined the angle by which any regular polygon with an even number of sides must be rotated about its centroid in order to maximise the volume of the three-dimensional solid obtained by revolving it \(180^\circ\) about the horizontal axis.
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.
Expository Writing
I really enjoy expository writing, because it allows me to demonstrate my point of view on mathematics that might already have been understood by people who... aren't me. Click on the links below to read my work!
Notes on Homological Algebra
MATH70063: Algebra 4 | Imperial College London, Winter 2024
Link to latest version of notes
A set of notes I am currently live-TeXing for a second-term Master's course on Homological Algebra taught by Oliver Gregory at Imperial in 2025.
Notes on Mathematical Logic
MATH70132: Lie Algebras | Imperial College London, Winter 2024
Link to latest version of notes
A set of notes I am currently live-TeXing for a second-term Master's course on Mathematical Logic taught by David Evans at Imperial in 2025.
Notes on Lie Algebras
MATH70062: Lie Algebras | Imperial College London, Winter 2024
Link to GitHub repository
A set of notes I live-TeXed for a first-term Master's course on Lie Algebras taught by Ambrus Pál at Imperial in 2024.
Notes on Representation Theory
MATH-314: Representation Theory of Finite Groups | EPFL, Spring 2024
Link to GitHub repository
A not-quite-complete set of notes I live-TeXed for a final-semester undergraduate course on Representation Theory taught by Aluna Rizzoli at EPFL in 2024.
Designing a Mathematical Mandala
Pages 43-47, Mathematics Today, April 2024
Link to Mathematics Today issues
In this article, I describe how to design a work of Mandala Art using relatively simple mathematics.
Talks
The only thing I enjoy more than writing about mathematics is speaking about mathematics. Public speaking comes naturally to me, and I have come to view technical presentations as a way of putting to test my ability to distill complicated ideas into their core components. I strive to structure my talks so that my audiences find them simple yet nontrivial. Enjoy!
Coxeter Groups
Imperial Undergraduate Mathematics Colloquium | Imperial College London, 2025
Link to talk recording
In the inaugural Spring 2025 talk of the Imperial Undergraduate Maths Colloquium, I discussed the fascinating subject of Coxeter groups. Coxeter groups are a special class of orthogonal transformations of Euclidean spaces. In my talk, I gave a very accessible overview of Coxeter groups, root systems, Coxeter graphs, and the general classification process of irreducible Coxeter groups. I also discussed the crystallographic case and the link to the classification of semi-simple Lie algebras over $\C$.
Designing a Mandala Using Mathematics
Warwick-Imperial Mathematics Conference | University of Warwick, 2024
Link to talk recording | Link to Desmos tutorial
The tradition of Mandala art goes back over a millennium, tracing its origin to the Indian subcontinent. Mandalas are characterised by layers of concentric circles with various motifs. The aesthetics tend to be pleasing to the eye due to certain symmetry properties of the motifs in question. In my talk, I explained how we can go the other way round to systematically build Mandalas by picking a desired symmetry group and designing motifs by plotting functions with appropriately fine-tuned parameters. My talk was based on an article I wrote for the April 2024 issue of Mathematics Today.
Partial Fraction Decomposition and its Formalisation in Lean
Tomorrow's Mathematicians Today | Institute for Mathematics and its Applications, 2023
Link to talk recording
In this talk, I presented my first significant Lean formalisation project, which I worked on as part of my Summer 2022 UROP.