2 papers
math.MG2026
Progress in Formalizing Sphere Packing in Dimension 8
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee +4
In 2016, Viazovska famously solved the sphere packing problem in dimension , using modular forms to construct a 'magic' function satisfying optimality conditions determined by C…
math.CO2021
Formalizing Hall's Marriage Theorem in Lean
Alena Gusakov, Bhavik Mehta, Kyle A. Miller
We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, which is a community-driven effort to build a unified mathematics library for Lean. One go…