论文标题
正式化Szemerédi的规律性引理和Roth的定理Isabelle/Hol
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
论文作者
论文摘要
我们使用证明助手isabelle/hol正式化了Szemerédi的规律性引理和Roth的定理，这是极端图理论和添加剂组合的两个主要结果。对于后一种形式化，我们使用前者首先显示三角计数引理和三角形去除引理：本身重要的技术结果。在这里，除了展示主要的正式陈述和定义外，我们还专注于证明中的敏感点，描述了我们如何克服遇到的困难。
We have formalised Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.
