# Formalizing the Solution to the Cap Set Problem

arXiv: https://arxiv.org/abs/1907.01449 · HTML: https://mlsanity.com/paper/1907.01449/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Jul 2019.

## Built on by (most cited first, 3 of 3)

- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Mathematical reasoning and the computer](https://mlsanity.com/paper/2502.07850/) (2025)
- [Notes on a Path to AI Assistance in Mathematical Reasoning](https://mlsanity.com/paper/2310.02896/) (2023)

## Abstract (arXiv)

In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of mathbbFnq 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 cap set problem. Ellenberg and Gijswijt's proof was published in the 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 mathbbFnq 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.