← All papers
Formalizing the Solution to the Cap Set Problem
cs.LO
Jul 2, 2019 · v1
TL;DR
Formalizes Ellenberg-Gijswijt's 2016 cap set bound proof in Lean.
Abstract
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of F_q^n with no three-term arithmetic progression. This problem has garnered significant mathematical attention, especially when q = 3, 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. We describe formalizing this proof in the Lean proof assistant, covering both the general result in F_q^n and concrete values for q = 3. We faithfully follow the pen and paper argument to construct the bound. The work demonstrates that some modern mathematics is within the range of proof assistants.
Problem
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of F_q^n with no three-term arithmetic progression (the cap set problem), but this result from the Annals of Mathematics had not been machine-verified.
Approach
The authors formalize Ellenberg and Gijswijt's proof of the cap set bound in the Lean proof assistant, covering both the general result in F_q^n and concrete values for q=3. The formalization faithfully follows the pen-and-paper argument, which is noteworthy for its clever use of elementary methods.
Results
The formalization demonstrates that modern mathematics published in top journals is within the range of proof assistants, providing a complete machine-checked proof of the cap set bound.