Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)

Author Angeliki Koutsoukou-Argyraki



PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.1.pdf
  • Filesize: 438 kB
  • 2 pages

Document Identifiers

Author Details

Angeliki Koutsoukou-Argyraki
  • University of Cambridge, UK

Cite AsGet BibTex

Angeliki Koutsoukou-Argyraki. Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.1

Abstract

In this talk, I will present an overview of recent formalisations, in the interactive theorem prover Isabelle/HOL, of significant theorems in additive combinatorics, an area of combinatorial number theory. The formalisations of these theorems were the first in any proof assistant to my knowledge. For each of these theorems, I will discuss selected aspects of the formalisation process, focussing on observations on our treatment of certain mathematical arguments when translated into Isabelle/HOL and our overall formalisation experience with Isabelle/HOL for this area of mathematics.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorics
  • Theory of computation → Logic and verification
Keywords
  • Additive combinatorics
  • additive number theory
  • combinatorial number theory
  • formalisation of mathematics
  • interactive theorem proving
  • proof assistants
  • Isabelle/HOL

Metrics

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

References

  1. Mantas Bakšys and Angeliki Koutsoukou-Argyraki. Kneser’s Theorem and the Cauchy-Davenport Theorem. Archive of Formal Proofs, November 2022. Formal proof development. URL: https://isa-afp.org/entries/Kneser_Cauchy_Davenport.html.
  2. Clemens Ballarin. A Case Study in Basic Algebra. Archive of Formal Proofs, August 2019. Formal proof development. URL: https://isa-afp.org/entries/Jacobson_Basic_Algebra.html.
  3. Matt DeVos. A Short Proof of Kneser’s Addition Theorem for Abelian Groups. In Springer Proceedings in Mathematics and Statistics, vol 101, pages 39-41, New York, NY, USA, 2014. Springer New York. URL: https://doi.org/10.1007/978-1-4939-1601-6_3.
  4. Chelsea Edmonds. Undirected Graph Theory. Archive of Formal Proofs, September 2022. Formal proof development. URL: https://isa-afp.org/entries/Undirected_Graph_Theory.html.
  5. Timothy Gowers. Introduction to Additive Combinatorics. Online course notes for Part III of the Mathematical Tripos, University of Cambridge, 2022. Google Scholar
  6. Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds. The Balog-Szemerédi-Gowers Theorem. Archive of Formal Proofs, November 2022. Formal proof development. URL: https://isa-afp.org/entries/Balog_Szemeredi_Gowers.html.
  7. Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds. A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Boston, MA, USA, pages 225-238, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575680.
  8. Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. Khovanskii’s Theorem. Archive of Formal Proofs, September 2022. Formal proof development. URL: https://isa-afp.org/entries/Khovanskii_Theorem.html.
  9. Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. The Plünnecke-Ruzsa Inequality. Archive of Formal Proofs, May 2022. Formal proof development. URL: https://isa-afp.org/entries/Pluennecke_Ruzsa_Inequality.html.
  10. Melvyn B. Nathanson. Additive Number Theory: The Classical Bases. Springer-Verlag New York, 1996. Google Scholar
  11. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL, A Proof Assistant for Higher-Order Logic. Springer-Verlag Berlin Heidelberg, 2002. Updated online tutorial on URL: https://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf.
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