License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.15
URN: urn:nbn:de:0030-drops-110703
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11070/
Go to the corresponding LIPIcs Volume Portal

Dahmen, Sander R. ; Hölzl, Johannes ; Lewis, Robert Y.

Formalizing the Solution to the Cap Set Problem

pdf-format:
LIPIcs-ITP-2019-15.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{dahmen_et_al:LIPIcs:2019:11070,
  author =	{Sander R. Dahmen and Johannes H{\"o}lzl and Robert Y. Lewis},
  title =	{{Formalizing the Solution to the Cap Set Problem}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11070},
  URN =		{urn:nbn:de:0030-drops-110703},
  doi =		{10.4230/LIPIcs.ITP.2019.15},
  annote =	{Keywords: formal proof, combinatorics, cap set problem, Lean}
}

Keywords: formal proof, combinatorics, cap set problem, Lean
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: Links to our formalization and supporting documents are hosted at the URL https://lean-forward.github.io/e-g/.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI