Upcoming Talks
Can Machines Pack Spheres?
Aarhus Math & AI Workshop | Aarhus Institute of Advanced Studies, January 2026
Progress on the Sphere Packing Formalisation Effort
Annual Meeting of the Swiss Mathematical Society | Brig, Switzerland, March 2026
Past Talks
Formally Packing 8-Dimensional Spheres
(Joint talk with Maryna Viazovska)
ItaLean 2025 | Bologna, Italy, 11 December 2025
Links to website
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.
The Road to Formalising 8-Dimensional Sphere Packing in Lean
Formalisation of Mathematics with Interactive Theorem Provers | University of Cambridge, 9 October 2025
Links to website and recording
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.
The Road to Formalising 8-Dimensional Sphere Packing in Lean
Graduate Student and Postdoc Seminar | Carnegie Mellon University, 11 September 2025
Link to recording
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.
Coxeter Groups
Imperial Undergraduate Mathematics Colloquium | Imperial College London, 15 January 2025
Link to 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 \(\mathbb{C}\).
Designing a Mandala Using Mathematics
Warwick-Imperial Mathematics Conference | University of Warwick, 23 November 2024
Links to recording and 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 recording
In this talk, I presented my first significant Lean formalisation project, which I worked on as part of my Summer 2022 UROP.