EPFL Packathon

Lausanne, 23–27 November 2026

EPFL Packathon

Let’s pack spheres in Lean!

theorem SpherePacking.MainTheorem : SpherePackingConstant 8 = E8Packing.density :=
  sorry
Dates
Monday 23 – Friday 27 November 2026
Venue
Bernoulli Center, EPFL, Lausanne
Deadline

Apply here

A circular line drawing: 240 points on eight concentric rings of thirty, joined by thousands of fine lines, with a red dot at the center.
240 minimal length vectors of E8 lattice.

About

The Sphere-Packing-Lean project formalizes the solution of the sphere packing problem in dimension 8 in Lean. Its Packathons are usually weekly online meetings. This one is in person: five days at the Bernoulli Center at EPFL, working on the formalization together.

The aim is to push the project forward: this is a working week, not a Lean tutorial. We expect most participants to have some formalization experience, but newcomers are welcome too. Most of each day is spent in working groups, listed on the Groups page. The week opens with introductory lectures on Monday and Tuesday. Some sessions will be hybrid, so people who can’t travel to Lausanne can join remotely.

Participation is primarily in person, by application until 30 October 2026, 23:59 CET. Accommodation is funded for all selected participants.

See the Lean Zulip announcement and discussion thread for more details.

Organizers