Formalizing the solution to the cap set problem

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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’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.

Original languageEnglish
Title of host publication10th International Conference on Interactive Theorem Proving (ITP 2019)
EditorsJohn Harrison, John O'Leary, Andrew Tolmach
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages1-19
Number of pages19
ISBN (Print)9783959771221
DOIs
Publication statusPublished - 2019
Event10th International Conference on Interactive Theorem Proving, ITP 2019 - Portland, United States
Duration: 9 Sep 201912 Sep 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume141
ISSN (Print)1868-8969

Conference

Conference10th International Conference on Interactive Theorem Proving, ITP 2019
CountryUnited States
CityPortland
Period9/09/1912/09/19

    Fingerprint

Keywords

  • Cap set problem
  • Combinatorics
  • Formal proof
  • Lean

Cite this

Dahmen, S. R., Hölzl, J., & Lewis, R. Y. (2019). Formalizing the solution to the cap set problem. In J. Harrison, J. O'Leary, & A. Tolmach (Eds.), 10th International Conference on Interactive Theorem Proving (ITP 2019) (pp. 1-19). [15] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 141). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ITP.2019.15