The Curious Case of Sphere Packing in Lean
Reflections on what the sphere packing project has taught us about large collaborative formalisation — and about how humans and machines can prove theorems together.
Expand for slides and more ↗
Progress in Formalizing Sphere Packing in Dimension 8
This talk is about the ongoing effort to formalise the solution the sphere packing problem in dimension 8. We discuss our progress this far, describe key design choices, reflect on significant milestones, and outline key objectives and challenges that remain. Based on joint work with Christopher Birkbeck, Seewoo Lee, Gareth Ma, Bhavik Mehta, Auguste Poiroux and Maryna Viazovska.
Expand for slides and more ↗
Large-Scale Formalisation: A Student's Perspective
In March 2024, when I was a third-year undergraduate exchange student in Switzerland, I embarked on a collaboration with Maryna Viazovska to formalise her seminal solution to the sphere packing problem in dimension 8. In this talk, I will reflect on the process of learning through formalisation, drawing on examples from my own work and beyond. I will furthermore describe the many milestones we have achieved over the course of the project, challenges unique to the formal medium, and objectives that remain. The sphere packing project is joint work with Christopher Birkbeck, Seewoo Lee, Gareth Ma, Bhavik Mehta, Maryna Viazovska, and community contributors.
Expand for slides and more ↗
A Lean Formalisation of Sphere Packing in Dimension 8
Arguably one of the most important sphere packing talks past and future, this talk was the first since the Gauss autoformalisation. I discussed progress made so far, commented briefly on the Gauss code, emphasised that the project was not over, and reflected on the ramifications for the future of formalised mathematics.
Expand for slides and more ↗
Can Machines Pack Spheres?
In this talk, I gave an update on the sphere packing formalisation and shared my experience attempting to "vibe-prove" that sphere packings in Euclidean spaces can be approximated arbitrarily well by lattice packings.
Expand for slides and more ↗
Formalising 8-Dimensional Sphere Packing in Lean
In this talk, we discussed the ongoing effort to formalise Maryna Viazovska's Fields medal work on Sphere Packings in \(8\) dimensions. We recapped the main achievements thus far and the problems that still remained.
Expand for slides and more ↗
Formally Packing 8-Dimensional Spheres
In this talk, we provided an introduction to the ongoing project to formalise Viazovska's solution to the sphere packing problem in dimension 8. We shared updates on our progress, outlined strategies to overcome remaining challenges, and discussed recent AI contributions to our project.
Expand for slides and more ↗
The Road to Formalising 8-Dimensional Sphere Packing in Lean
In this talk, I presented my ongoing work on formalising the packing of 8-dimensional spheres in the Lean theorem prover. I discussed progress and challenges and outlined avenues for community contributions.
Expand for slides and more ↗
The Road to Formalising 8-Dimensional Sphere Packing in Lean
In this talk, I presented my ongoing work on formalising the packing of 8-dimensional spheres in the Lean theorem prover. I discussed progress and challenges and outlined avenues for community contributions.
Expand for slides and more ↗
Coxeter Groups
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 \(\mathbb{C}\).
Designing a Mandala Using Mathematics
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
In this talk, I presented my first significant Lean formalisation project, which I worked on as part of my Summer 2022 UROP.
Expand for slides and more ↗