Conferences & Workshops
Events I've organised, or helped organise.
EPFL Packathon
Five days of formalising sphere packing in Lean at the Bernoulli Center at EPFL: an in-person working week for the Sphere-Packing-Lean project, which is formalising the solution of the sphere packing problem in dimension 8.
It is an in-person edition of our weekly packathons. Most of each day is spent in working groups — on contour integration, analytic continuation, upstreaming to Mathlib, metaprogramming, autoformalisation with AI tools in SphereCeti, and a collection of self-contained target statements for newcomers. The week opens with introductory lectures on the Monday and Tuesday (the first by Chris Birkbeck, Seewoo Lee and me), and some sessions are hybrid, so that people who can't travel to Lausanne can join remotely.
Tutorials/Demonstrations
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.
A brief introduction to Lean
A pop-up Lean tutorial offering a brief and practical introduction to Lean.
Working Groups
Great minds work best together!
Weekly Packathons
Every Monday at 11 am Eastern Time, we have a 'packathon' (in-person at the Hoskinson Center at CMU and virtually on Zoom) where anyone interested in the sphere packing formalisation can show up, talk about their work, exchange ideas, and collaborate! If you'd like to join us, check out the Zulip thread (or send me an email)!
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.