Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL

DOI10.1007/s10817-022-09650-2arXiv2207.07499WikidataQ124823534 ScholiaQ124823534MaRDI QIDQ6156630

Angeliki Koutsoukou-Argyraki, Lawrence Charles Paulson, Chelsea Edmonds

Publication date: 14 June 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2207.07499

zbMATH Keywords

arithmetic progressionsextremal graph theorynumber theoryproof assistantadditive combinatoricsformalisation of mathematicsIsabelle/HOLinteractive theorem proving

Mathematics Subject Classification ID

Extremal problems in graph theory (05C35) Combinatorial aspects of partitions of integers (05A17) Mechanization of proofs and logical operations (03B35) Elementary theory of partitions (11P81) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Digital mathematics libraries and repositories (68V35)

Related Items (1)

Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

Cites Work

• Unnamed Item
• Unnamed Item
• The Green-Tao theorem: an exposition
• Ergodic behavior of diagonal measures and a theorem of Szemeredi on arithmetic progressions
• Lower bounds of tower type for Szemerédi's uniformity lemma
• Isabelle/HOL. A proof assistant for higher-order logic
• A graph library for Isabelle
• A modular first formalisation of combinatorial design theory
• The primes contain arbitrarily long arithmetic progressions
• Hypergraph regularity and the multidimensional Szemerédi theorem
• Graph Theory
• Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem
• Quasirandomness, Counting and Regularity for 3-Uniform Hypergraphs
• On sets of integers containing k elements in arithmetic progression
• Extremal problems on set systems
• Regularity Lemma for k-uniform hypergraphs
• Formalizing Ordinal Partition Relations Using Isabelle/HOL
• Regularity lemmas for stable graphs
• Interview with Endre Szemerédi
• Erdős and Arithmetic Progressions
• The counting lemma for regular k‐uniform hypergraphs
• On Certain Sets of Integers
• A new proof of Szemerédi's theorem

This page was built for publication: Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL