Right now
I'm on vacation until 11 July 2026.
Travel
Where I'll be — and where I've been.
Coming up
-
27 Jun 2026 – 11 Jul 2026
On vacation
-
12 Jul 2026 – 18 Jul 2026
AI and Mathematics: Formalization, Theorem Proving, and Reasoning — Korea Institute for Advanced Study, Seoul, South Korea ↗
🎤 Giving a talk:
Large-Scale Formalisation: A Student's Perspective
Monday, 13 July 2026 • 09:30 local time (00:30 UTC)
In this talk, I share a student's perspective on what it's like to work on a large-scale, community-driven formalisation project. Drawing on my experience with the sphere packing formalisation, I discuss the practicalities of contributing to and coordinating large Lean developments, the role of AI tooling in accelerating this work, and what such projects can teach early-career researchers about modern mathematical practice.
-
20 Jul 2026 – 23 Jul 2026
International Congress on Mathematical Software (ICMS) — Waterloo (ON), Canada ↗
🎤 Giving a talk:
Progress in Formalizing Sphere Packing in Dimension 8
A look at the effort to formalise Viazovska's solution to the sphere packing problem in dimension 8, what has been achieved so far, and what this milestone means for the future of computer-verified mathematics.
-
24 Jul 2026 – 29 Jul 2026
International Congress of Mathematicians (ICM) — Philadelphia (PA), United States ↗
-
25 Jul 2026
Workshop affiliated to the 17th International Conference on Interactive Theorem Proving (ITP) and the Federated Logic Conferences (FLoC) (virtual) — Lisbon, Portugal ↗
🎤 Giving a virtual talk:
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.
-
3 Aug 2026 – 8 Aug 2026
Tata Institute for Fundamental Research — Mumbai, India ↗
🎤 Giving a talk:
Formalisation in the Age of AI: The Learnings of a Sphere Packer
In this talk, I reflect on the learnings from the sphere packing formalisation project in the age of AI. I discuss how machine learning and AI-assisted proof techniques have transformed the landscape of formal mathematics, the opportunities and challenges they present, and what the sphere packing journey has taught us about the future of computer-verified mathematics.
Been there
-
25 Mar 2026 – 27 Mar 2026
Swiss Mathematical Society Spring Meeting: Formalisation and Proof Assistants — UniDistance Suisse, Brig (VS), Switzerland ↗
🎤 Gave a talk:
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.
-
23 Mar 2026 – 24 Mar 2026
Academic Visit — EPFL, Ecublens (VD), Switzerland
-
9 Dec 2025 – 12 Dec 2025
ItaLean — Bologna, Italy ↗
🎤 Gave a talk:
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.
🧩 Led a working group here:
Sphere Packing Working Group
In December 2025, I led a working group of interested formalisers at ItaLean in Bologna to make progress on the formalisation of the 8-dimensional sphere packing problem in Lean.
-
9 Oct 2025
Formalisation of Mathematics with Interactive Theorem Provers — University of Cambridge, Cambridge, United Kingdom ↗
🎤 Gave a talk:
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.
-
15 Sep 2025 – 19 Sep 2025
Mechanization and Mathematical Research — Leiden, Netherlands ↗
Took part in the initial discussions that led to the drafting of the Leiden Declaration on AI and Mathematics, of which I am a signatory.
-
9 Jun 2025 – 13 Jun 2025
Big Proof 2025 — Cambridge, United Kingdom ↗