Groups
| Topic | Description |
|---|---|
| Contour integration | Prove general versions of the Cauchy–Goursat theorem, the residue theorem and other key results on contour integration: general results for Mathlib, and the specific ones the project needs to compute the Fourier transforms of the pieces of the magic function. |
| Analytic continuation | Some integral formulas for the magic function converge only for r > √2. Prove that they extend to smaller r by analytic continuation, which the proof needs for the values near the origin. |
| Mathlib upstreaming | Generalize the parts of the project that are useful beyond sphere packing, such as modular forms and Fourier analysis, and upstream them to Mathlib. This may mean redesigning some definitions and API, bringing the code up to Mathlib standards and taking it through review. |
| Metaprogramming | Develop tactics and other Lean metaprogramming to automate the routine steps of proofs. One specific goal is a tactic for computing integrals, which can be tedious to do by hand in Lean. |
| SphereCeti | An experiment in autoformalization, working with AI tools in the SphereCeti repository. SphereCeti is meant to be to the sphere packing project what Tau Ceti is to Mathlib. |
| Target practice | Before the workshop, we will add a collection of self-contained target statements to the repository. Pick one and prove it! Open to all levels, and a good way in for people new to the project. |
Notes
This list is indicative: groups may be merged or subdivided, and new ones added. Suggestions are welcome.
Before the workshop, we will add precisely stated targets to the repository and update the blueprint and project dashboard, so that groups can start right away.