Formalizing the Solution to the Cap Set Problem

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

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 m…