Application

The Packathon is about making progress on the Sphere Packing in Lean project, not a Lean tutorial. We expect most participants to have some formalization experience, but newcomers are welcome too: the target statements of the target practice group are a good way into the project.

Working groups: contour integration; analytic continuation of the magic function; Mathlib upstreaming; metaprogramming (for example, a tactic for integral computations); SphereCeti; target practice (proving self-contained target statements). See the Groups page for details. You can also propose your own.

Accommodation is funded for all selected participants. Travel funding is handled case by case; it is not guaranteed.

• Name and institution
• Your Lean experience (self-reported) and a short motivation statement
• Which working groups interest you
• A CV (uploading it requires signing in to a Google account), your GitHub username and links to previous work
• Practical details: accommodation, arrival and departure dates, travel reimbursement and approximate cost, dietary requirements