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

Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson

Research output: Contribution to journalArticlepeer-review

Original languageEnglish
Article number2
Number of pages21
JournalJournal of Automated Reasoning
Volume67
Issue number1
DOIs
Publication statusPublished - 19 Dec 2022

Keywords

  • Additive combinatorics
  • Arithmetic progressions
  • Extremal graph theory
  • Formalisation of mathematics
  • Interactive theorem proving
  • Isabelle/HOL
  • Number theory
  • Proof assistant

Cite this