@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",

}