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…
cs.FL2025
A complete formalization of Fermat's Last Theorem for regular primes in Lean
Alex Best, Christopher Birkbeck, Riccardo Brasca +3
We formalize a complete proof of the regular case of Fermat's Last Theorem in the Lean4 theorem prover. Our formalization includes a proof of Kummer's lemma, that is the main obstr…