Showing 1–3 of 3 results for author: Birkbeck, C

Progress in Formalizing Sphere Packing in Dimension 8

Authors: Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska

Abstract: In 2016, Viazovska famously solved the sphere packing problem in dimension $8$, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 202… ▽ More In 2016, Viazovska famously solved the sphere packing problem in dimension $8$, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain. △ Less

Submitted 29 May, 2026; v1 submitted 25 April, 2026; originally announced April 2026.

Comments: 8 pages, title updated

A complete formalization of Fermat's Last Theorem for regular primes in Lean

Authors: Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van De Velde, Andrew Yang

Abstract: 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 obstruction to Fermat's Last Theorem for regular primes. Rather than following the modern proof of Kummer's lemma via class field theory, we prove it by using Hilbert's Theorems 90-94 in a way that is more amenable to formali… ▽ More 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 obstruction to Fermat's Last Theorem for regular primes. Rather than following the modern proof of Kummer's lemma via class field theory, we prove it by using Hilbert's Theorems 90-94 in a way that is more amenable to formalization. △ Less

Submitted 13 June, 2025; v1 submitted 2 October, 2024; originally announced October 2024.

Fermat's Last Theorem for regular primes

Authors: Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi

Abstract: We formalise the proof of the first case of Fermat's Last Theorem for regular primes using the \emph{Lean} theorem prover and its mathematical library \emph{mathlib}. This is an important 19th century result that motivated the development of modern algebraic number theory. Besides explaining the mathematics behind this result, we analyze in this paper the difficulties we faced in the formalisation… ▽ More We formalise the proof of the first case of Fermat's Last Theorem for regular primes using the \emph{Lean} theorem prover and its mathematical library \emph{mathlib}. This is an important 19th century result that motivated the development of modern algebraic number theory. Besides explaining the mathematics behind this result, we analyze in this paper the difficulties we faced in the formalisation process and how we solved them. For example, we had to deal with a diamond about characteristic zero fields and problems arising from multiple nested coercions related to number fields. We also explain how we integrated our work to \emph{mathlib}. △ Less

Submitted 21 May, 2023; v1 submitted 15 May, 2023; originally announced May 2023.

Comments: Accepted for the 14th International Conference on Interactive Theorem Proving (ITP 2023)

MSC Class: 68V20; 03B70 ACM Class: F.4.1