Where in the world?

Where I am right now — and where I'll be next.

Right now

I'm doing an internship at Axiom Math in Palo Alto (CA), United States until 21 August 2026.

Travel

Where I'll be — and where I've been, newest first.

  1. Today — 8 August 2026

  2. 3 Aug 2026 – 7 Aug 2026

    AI for Mathematics Workshop — Tata Institute of Fundamental Research, Mumbai (MH), India ↗

    🎤 Gave a talk:

    Verification, Formalisation and Canonisation: Formal Theorem Proving in the Age of AI

    Interactive Theorem Provers and AI have both risen to prominence concurrently and complementarily: the confidence offered by the formal paradigm strongly incentivises training, benchmarking and deploying models to reason formally, and improvements in AI are strongly influencing the development of formal mathematics. The demand for formal verification has never been greater. Yet, while AI models are proving themselves increasingly capable of autonomously verifying proofs in interactive theorem provers like Lean, they continue to depend heavily on over a decade’s worth of formal infrastructure built through open-source collaboration and carefully curated by human maintainers. For formal mathematics to develop sustainably, important (if subtle) distinctions must be drawn between formal verification and canonisation. While both serve valuable purposes, these purposes are distinct, and the capabilities of models to serve them differ starkly. My talk will explore the nuances of doing formal mathematics in the age of AI, motivated and illustrated largely by joint work on formalising sphere packing in dimension 8 with Birkbeck, Lee, Ma, Mehta, Poiroux and Viazovska.

    See this talk →

    📚 Gave a tutorial here:

    A practical introduction to theorem proving and formalisation in Lean

    A comprehensive, hands-on Lean tutorial spanning 8 hours over 4 sessions over 2 days. I briefly introduced important foundational properties that practically affect the way theorems and proofs are written in Lean; demonstrated various tactics; introduced different ways of writing definitions (such as structures and typeclasses); and explained important design choices and conventions (general and domain-specific) in Mathlib and downstream projects. I also talked a bit about how to get involved in open-source projects and shared some tips and pitfalls (with a brief demonstration) of using frontier LLMs for formalisation.

    See this tutorial →

  3. 25 Jul 2026

    Workshop affiliated to the 17th International Conference on Interactive Theorem Proving (ITP) and the Federated Logic Conferences (FLoC) (virtual) — Lisbon, Portugal ↗

    🎤 Gave a virtual talk:

    The Curious Case of Sphere Packing in Lean

    This talk is about recent progress in the sphere packing project, with particular emphasis on the unique challenge of balancing progress towards finishing the project and cleaning up an AI-generated formal verification. We reflect on the successes and failures of this process and its implications for the future of AI-generated formal mathematics, particularly reflecting on what distinguishes a formal verification from a true formalisation.

    See this talk →

  4. 24 Jul 2026 – 29 Jul 2026

    International Congress of Mathematicians (ICM) — Philadelphia (PA), United States ↗

  5. 20 Jul 2026 – 23 Jul 2026

    International Congress on Mathematical Software (ICMS) — Waterloo (ON), Canada ↗

    🎤 Gave a talk:

    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.

    See this talk →

  6. 12 Jul 2026 – 18 Jul 2026

    AI and Mathematics: Formalization, Theorem Proving, and Reasoning — Korea Institute for Advanced Study, Seoul, South Korea ↗

    🎤 Gave a talk:

    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.

    See this talk →

    📚 Gave a tutorial here:

    A brief introduction to Lean

    A pop-up Lean tutorial offering a brief and practical introduction to Lean.

    See this tutorial →

  7. 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.

    See this talk →

  8. 23 Mar 2026 – 24 Mar 2026

    Academic Visit — EPFL, Ecublens (VD), Switzerland

  9. 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.

    See this talk →

    🧩 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.

    See this working group →

  10. 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.

    See this talk →

  11. 15 Sep 2025 – 19 Sep 2025

    Mechanization and Mathematical Research — Lorentz Center, 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.

  12. 9 Jun 2025 – 13 Jun 2025

    Big Proof 2025 — Isaac Newton Institute, Cambridge, United Kingdom ↗