License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.1
URN: urn:nbn:de:0030-drops-183760
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18376/
Go to the corresponding LIPIcs Volume Portal

Koutsoukou-Argyraki, Angeliki

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

pdf-format:
LIPIcs-ITP-2023-1.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{koutsoukouargyraki:LIPIcs.ITP.2023.1,
  author =	{Koutsoukou-Argyraki, Angeliki},
  title =	{{Formalisation of Additive Combinatorics in Isabelle/HOL}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18376},
  URN =		{urn:nbn:de:0030-drops-183760},
  doi =		{10.4230/LIPIcs.ITP.2023.1},
  annote =	{Keywords: Additive combinatorics, additive number theory, combinatorial number theory, formalisation of mathematics, interactive theorem proving, proof assistants, Isabelle/HOL}
}

Keywords: Additive combinatorics, additive number theory, combinatorial number theory, formalisation of mathematics, interactive theorem proving, proof assistants, Isabelle/HOL
Collection: 14th International Conference on Interactive Theorem Proving (ITP 2023)
Issue Date: 2023
Date of publication: 26.07.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI