eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
15:1
15:19
10.4230/LIPIcs.ITP.2019.15
article
Formalizing the Solution to the Cap Set Problem
Dahmen, Sander R.
1
https://orcid.org/0000-0002-0014-0789
Hölzl, Johannes
2
https://orcid.org/0000-0003-0869-9250
Lewis, Robert Y.
2
https://orcid.org/0000-0002-5266-1121
Department of Mathematics, Vrije Universiteit Amsterdam, The Netherlands
Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of 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 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 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.15/LIPIcs.ITP.2019.15.pdf
formal proof
combinatorics
cap set problem
Lean