@inproceedings{e91f789cd5a14ed6a55ad4858bb60365,
title = "Formalizing the solution to the cap set problem",
abstract = "In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of 픽nq 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{\textquoteright}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 픽nq 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.",
keywords = "Cap set problem, Combinatorics, Formal proof, Lean",
author = "Dahmen, {Sander R.} and Johannes H{\"o}lzl and Lewis, {Robert Y.}",
year = "2019",
doi = "10.4230/LIPIcs.ITP.2019.15",
language = "English",
isbn = "9783959771221",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
pages = "1--19",
editor = "John Harrison and John O'Leary and Andrew Tolmach",
booktitle = "10th International Conference on Interactive Theorem Proving (ITP 2019)",
note = "10th International Conference on Interactive Theorem Proving, ITP 2019 ; Conference date: 09-09-2019 Through 12-09-2019",
}