Formalizing the Solution to the Cap Set Problem

DOI10.4230/LIPICS.ITP.2019.15MaRDI QIDQ6321422arXivFDO

Authors Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis

Publication date 2 July 2019

Published in arXiv

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2019.15

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

arXiv classification

cs.LOmath.CO

Abstract: In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $mathbb{F}_q^n$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q=3$, where it is commonly known as the emph{cap set problem}. Ellenberg and Gijswijt's proof was published in the emph{Annals of Mathematics} and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in $mathbb{F}_q^n$ and concrete values for the case $q=3$. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.

This page was built for publication: Formalizing the Solution to the Cap Set Problem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6321422)