在 Isabelle/HOL 中形式化 Szemerédi 正则引理与 Roth 算术级数定理
计算机科学中的逻辑
2022-10-14 v3
摘要
我们使用证明辅助工具 Isabelle/HOL 形式化了 Szemerédi 正则引理与 Roth 算术级数定理，这两个是极值图论与加性组合学中的重大结果。对于后者的形式化，我们利用前者首先证明了三角计数引理与三角移除引理：它们本身也是重要的技术结果。在此，除了展示主要的形式化陈述与定义外，我们聚焦于证明中的关键难点，描述我们如何克服所遇到的困难。
引用
@article{arxiv.2207.07499,
title = {Formalising Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL},
author = {Chelsea Edmonds and Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson},
journal= {arXiv preprint arXiv:2207.07499},
year = {2022}
}