Document Open Access Logo

Formalizing the Solution to the Cap Set Problem

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

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Sander R. Dahmen
  • Department of Mathematics, Vrije Universiteit Amsterdam, The Netherlands
Johannes Hölzl
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
Robert Y. Lewis
  • Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands

Funding

  • Dahmen, Sander R.: NWO Vidi grant No. 639.032.613, New Diophantine Directions
  • Hölzl, Johannes: ERC grant agreement No. 713999, Matryoshka
  • Lewis, Robert Y.: ERC grant agreement No. 713999, Matryoshka

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 AsGet BibTex

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
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact