LIPIcs.ITP.2023.1.pdf
- Filesize: 438 kB
- 2 pages
Document
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
Author
Angeliki Koutsoukou-Argyraki 
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
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
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)
0PDF Downloads
References
- 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.
- 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.
- 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.
- Chelsea Edmonds. Undirected Graph Theory. Archive of Formal Proofs, September 2022. Formal proof development. URL: https://isa-afp.org/entries/Undirected_Graph_Theory.html.
-
Timothy Gowers. Introduction to Additive Combinatorics. Online course notes for Part III of the Mathematical Tripos, University of Cambridge, 2022.
- 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.
- 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.
- 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.
- 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.
-
Melvyn B. Nathanson. Additive Number Theory: The Classical Bases. Springer-Verlag New York, 1996.
- 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.