Document

# Formalizing the Solution to the Cap Set Problem

## File

LIPIcs.ITP.2019.15.pdf
• Filesize: 0.51 MB
• 19 pages

## Acknowledgements

We are grateful to the Lean mathlib maintainers and contributors on whose work this project is based. We thank Jeremy Avigad and Jasmin Blanchette for helpful comments on this paper, Dion Gijswijt for suggesting an improvement to our asymptotic bound argument, and Manuel Eberl for pointing us to related work.

## Cite As

Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.15

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

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Logic and verification
• Theory of computation → Type theory
• Mathematics of computing → Number-theoretic computations
• Computing methodologies → Combinatorial algorithms
• Software and its engineering → Formal methods
##### Keywords
• formal proof
• combinatorics
• cap set problem
• Lean

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. Journal of Formalized Reasoning, October 2018. URL: https://hal.inria.fr/hal-01719918.
2. Jesús Aransay and Jose Divasón. Formalization and Execution of Linear Algebra: From Theorems to Algorithms. In Gopal Gupta and Ricardo Peña, editors, Logic-Based Program Synthesis and Transformation, pages 1-18, Cham, 2014. Springer International Publishing.
3. Sophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub. Formal Proofs of Transcendence for e and Pi As an Application of Multivariate and Symmetric Polynomials. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pages 76-87, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2854065.2854072.
4. Mario Carneiro. The Lean 3 Mathematical Library (presentation), July 2018. URL: http://robertylewis.com/files/icms/Carneiro_mathlib.pdf.
5. Hing-Lun Chan and Michael Norrish. Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving, pages 117-136, Cham, 2015. Springer International Publishing.
6. Hing-Lun Chan and Michael Norrish. Proof Pearl: Bounding Least Common Multiples with Triangles. In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem Proving, pages 140-150, Cham, 2016. Springer International Publishing.
7. Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi. A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 160-176, Cham, 2014. Springer International Publishing.
8. Thierry Coquand and Christine Paulin. Inductively defined types. In COLOG-88 (Tallinn, 1988), volume 417 of Lec. Notes in Comp. Sci., pages 50-66. Springer, Berlin, 1990. URL: https://doi.org/10.1007/3-540-52335-9_47.
9. Ernie Croot, Vsevolod F. Lev, and Péter Pál Pach. Progression-free sets in ℤⁿ₄ are exponentially small. Ann. of Math. (2), 185(1):331-337, 2017. URL: https://doi.org/10.4007/annals.2017.185.1.7.
10. N. G. de Bruijn. AUTOMATH, a Language for Mathematics. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pages 159-200. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_11.
11. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover, 2014. URL: http://leanprover.github.io/files/system.pdf.
12. Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada. A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 17-29, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3018610.3018617.
13. Jose Divasón and Jesús Aransay. Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs, January 2013. Formal proof development. URL: http://isa-afp.org/entries/Rank_Nullity_Theorem.html.
14. Catherine Dubois, Alain Giorgetti, and Richard Genestier. Tests and Proofs for Enumerative Combinatorics. In Bernhard K. Aichernig and Carlo A. Furia, editors, Tests and Proofs, pages 57-75, Cham, 2016. Springer International Publishing.
15. Manuel Eberl. Symmetric Polynomials. Archive of Formal Proofs, September 2018. Formal proof development. URL: http://isa-afp.org/entries/Symmetric_Polynomials.html.
16. Manuel Eberl. Nine Chapters of Analytic Number Theory in Isabelle/HOL. In Interactive Theorem Proving, 2019.
17. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metaprogramming framework for formal verification. Proceedings of the ACM on Programming Languages, 1(ICFP):34, 2017.
18. Jordan S. Ellenberg and Dion Gijswijt. On large subsets of 𝔽ⁿ_q with no three-term arithmetic progression. Ann. of Math. (2), 185(1):339-343, 2017. URL: https://doi.org/10.4007/annals.2017.185.1.8.
19. Georges Gonthier. The Four Colour Theorem: Engineering of a Formal Proof. In Deepak Kapur, editor, Computer Mathematics, pages 333-333, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
20. Georges Gonthier. Point-Free, Set-Free Concrete Linear Algebra. In Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving, pages 103-118, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.
21. Sébastien Gouëzel and Vladimir Shchur. A corrected quantitative version of the Morse lemma. arXiv preprint, 2018. URL: http://arxiv.org/abs/1810.04579.
22. Larry Guth. Polynomial methods in combinatorics, volume 64 of University Lecture Series. American Mathematical Society, Providence, RI, 2016.
23. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the Kepler conjecture. In Forum of Mathematics, Pi, volume 5. Cambridge University Press, 2017.
24. John Harrison. The HOL Light Theory of Euclidean Space. J. Autom. Reason., 50(2):173-190, February 2013. URL: https://doi.org/10.1007/s10817-012-9250-9.
25. Holden Lee. Vector Spaces. Archive of Formal Proofs, August 2014. Formal proof development. URL: http://isa-afp.org/entries/VectorSpace.html.
26. Robert Y. Lewis. A Formal Proof of Hensel’s lemma over the p-adic Integers. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 15-26, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3293880.3294089.
27. Roman Matuszewski and Piotr Rudnicki. Mizar: the first 30 years. Mechanized Mathematics and Its Applications, 4(1):3-24, March 2005.
28. Bas Spitters and Eelis van der Weegen. Type classes for mathematics in type theory. Mathematical Structures in Computer Science, 21(4):795-825, 2011.
29. Terence Tao. Algebraic combinatorial geometry: the polynomial method in arithmetic combinatorics, incidence combinatorics, and number theory. EMS Surv. Math. Sci., 1(1):1-46, 2014. URL: https://doi.org/10.4171/EMSS/1.
30. Terence Tao. A symmetric formulation of the Croot-Lev-Pach-Ellenberg-Gijswijt capset bound, May 2016. URL: http://terrytao.wordpress.com/2016/05/18.
31. Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. Homotopy Type Theory in Lean. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, pages 479-495. Springer International Publishing, 2017.
32. P. Wadler and S. Blott. How to Make Ad-hoc Polymorphism Less Ad Hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '89, pages 60-76, New York, NY, USA, 1989. ACM. URL: https://doi.org/10.1145/75277.75283.
33. Doron Zeilberger. A Motivated Rendition of the Ellenberg-Gijswijt Gorgeous proof that the Largest Subset of F₃ⁿ with No Three-Term Arithmetic Progression is O (cⁿ), with c = ∛(5589+891√33)/8 = 2.75510461302363300022127…. arXiv preprint, 2016. URL: http://arxiv.org/abs/1607.01804.
X

Feedback for Dagstuhl Publishing