  In 2016, Ellenberg and Gijswijt established a new upper bound on the size of
subsets of $\mathbb{F}^n_q$ 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}^n_q$ 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.
