eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
1:1
1:2
10.4230/LIPIcs.ITP.2023.1
article
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
Koutsoukou-Argyraki, Angeliki
1
https://orcid.org/0000-0002-8886-5281
University of Cambridge, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.1/LIPIcs.ITP.2023.1.pdf
Additive combinatorics
additive number theory
combinatorial number theory
formalisation of mathematics
interactive theorem proving
proof assistants
Isabelle/HOL