{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:06:15Z","timestamp":1746745575618,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,12,19]],"date-time":"2022-12-19T00:00:00Z","timestamp":1671408000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,12,19]],"date-time":"2022-12-19T00:00:00Z","timestamp":1671408000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We have formalised Szemer\u00e9di\u2019s Regularity Lemma and Roth\u2019s 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.<\/jats:p>","DOI":"10.1007\/s10817-022-09650-2","type":"journal-article","created":{"date-parts":[[2022,12,19]],"date-time":"2022-12-19T05:02:40Z","timestamp":1671426160000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalising Szemer\u00e9di\u2019s Regularity Lemma and Roth\u2019s Theorem on Arithmetic Progressions in Isabelle\/HOL"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8559-9133","authenticated-orcid":false,"given":"Chelsea","family":"Edmonds","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8886-5281","authenticated-orcid":false,"given":"Angeliki","family":"Koutsoukou-Argyraki","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,19]]},"reference":[{"key":"9650_CR1","unstructured":"Bell, S., Grodzicki, W.: Using Szemer\u00e9di\u2019s regularity lemma to prove Roth\u2019s theorem. Lecture notes. University of Georgia (2010)"},{"key":"9650_CR2","unstructured":"Buzzard, K.: What is the point of computers? A question for pure mathematicians. In: Proceedings of the international congress of mathematicians (ICM 2022) (2022). arXiv:2112.11598"},{"key":"9650_CR3","doi-asserted-by":"publisher","first-page":"03","DOI":"10.4171\/EMSS\/6","volume":"1","author":"D Conlon","year":"2014","unstructured":"Conlon, D., Fox, J., Zhao, Y.: The Green-Tao theorem: an exposition. EMS Surv. Math. Sci. 1, 03 (2014)","journal-title":"EMS Surv. Math. Sci."},{"key":"9650_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53622-3","volume-title":"Graph Theory","author":"R Diestel","year":"2017","unstructured":"Diestel, R.: Graph Theory. Springer, Cham (2017)"},{"key":"9650_CR5","unstructured":"Dillies, Y.,\u00a0Mehta, B.: Formalizing Szemer\u00e9di\u2019s regularity lemma in Lean. In: Andronick, J., de\u00a0Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"9650_CR6","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2021.1980464","author":"M D\u017eamonja","year":"2022","unstructured":"D\u017eamonja, M., Koutsoukou-Argyraki, A., Paulson, L.C.: Formalising ordinal partition relations using Isabelle\/HOL. Exp. Math. (2022). https:\/\/doi.org\/10.1080\/10586458.2021.1980464","journal-title":"Exp. Math."},{"key":"9650_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-81097-9_1","volume-title":"Intelligent Computer Mathematics","author":"C Edmonds","year":"2021","unstructured":"Edmonds, C., Paulson, L.C.: A modular first formalisation of combinatorial design theory. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) Intelligent Computer Mathematics, pp. 3\u201318. Springer, Cham (2021)"},{"key":"9650_CR8","unstructured":"Edmonds, C., Paulson, L.C.: Fisher\u2019s inequality: Linear algebraic proof techniques for combinatorics. Archive of Formal Proofs. (2022). https:\/\/isa-afp.org\/entries\/Fishers_Inequality.html"},{"key":"9650_CR9","unstructured":"Edmonds, C.,\u00a0Koutsoukou-Argyraki, A., Paulson, L.C.: Roth\u2019s theorem on arithmetic progressions. Archive of Formal Proofs. Formal proof development. (2021). https:\/\/isa-afp.org\/entries\/Roth_Arithmetic_Progressions.html"},{"key":"9650_CR10","unstructured":"Edmonds, C.,\u00a0Koutsoukou-Argyraki, A., Paulson, L.C.: Szemer\u00e9di\u2019s regularity lemma. Archive of Formal Proofs (2021). https:\/\/isa-afp.org\/entries\/Szemeredi_Regularity.html"},{"issue":"4","key":"9650_CR11","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1112\/jlms\/s1-11.4.261","volume":"s1\u201311","author":"P Erd\u0151s","year":"1936","unstructured":"Erd\u0151s, P., Tur\u00e1n, P.: On some sequences of integers. J. Lond. Math. Soc. s1\u201311(4), 261\u2013264 (1936)","journal-title":"J. Lond. Math. Soc."},{"issue":"2","key":"9650_CR12","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1002\/rsa.10017","volume":"20","author":"P Frankl","year":"2002","unstructured":"Frankl, P., R\u00f6dl, V.: Extremal problems on set systems. Random Struct. Algorithms 20(2), 131\u2013164 (2002)","journal-title":"Random Struct. Algorithms"},{"issue":"1","key":"9650_CR13","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/BF02813304","volume":"31","author":"H Furstenberg","year":"1977","unstructured":"Furstenberg, H.: Ergodic behavior of diagonal measures and a theorem of Szemer\u00e9di on arithmetic progressions. Journal d\u2019Analyse Math\u00e9matique 31(1), 204\u2013256 (1977)","journal-title":"Journal d\u2019Analyse Math\u00e9matique"},{"key":"9650_CR14","unstructured":"Gouezel, S.: Ergodic theory. Archive of Formal Proofs. (2015) https:\/\/isa-afp.org\/entries\/Ergodic_Theory.html"},{"key":"9650_CR15","unstructured":"Gowers, W.T.: Topics in combinatorics. (Notes taken by Paul Russell).(2004) https:\/\/www.dpmms.cam.ac.uk\/~par31\/notes\/tic.pdf"},{"issue":"2","key":"9650_CR16","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/PL00001621","volume":"7","author":"WT Gowers","year":"1997","unstructured":"Gowers, W.T.: Lower bounds of tower type for Szemer\u00e9di\u2019s uniformity lemma. Geom. Funct. Anal. GAFA 7(2), 322\u2013337 (1997)","journal-title":"Geom. Funct. Anal. GAFA"},{"issue":"3","key":"9650_CR17","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s00039-001-0332-9","volume":"11","author":"WT Gowers","year":"2001","unstructured":"Gowers, W.T.: A new proof of Szemer\u00e9di\u2019s theorem. Geom. Funct. Anal. GAFA 11(3), 465\u2013588 (2001)","journal-title":"Geom. Funct. Anal. GAFA"},{"issue":"1\u20132","key":"9650_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1017\/S0963548305007236","volume":"15","author":"WT Gowers","year":"2006","unstructured":"Gowers, W.T.: Quasirandomness, counting and regularity for 3-uniform hypergraphs. Comb. Probab. Comput. 15(1\u20132), 143\u2013184 (2006)","journal-title":"Comb. Probab. Comput."},{"issue":"3","key":"9650_CR19","doi-asserted-by":"publisher","first-page":"897","DOI":"10.4007\/annals.2007.166.897","volume":"166","author":"WT Gowers","year":"2007","unstructured":"Gowers, W.T.: Hypergraph regularity and the multidimensional Szemer\u00e9di theorem. Ann. Math. 166(3), 897\u2013946 (2007)","journal-title":"Ann. Math."},{"key":"9650_CR20","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-39286-3_8","volume-title":"Erd\u0151s Centennial","author":"WT Gowers","year":"2013","unstructured":"Gowers, W.T.: Erd\u0151s and arithmetic progressions. In: Lov\u00e1sz, L., Ruzsa, I.Z., S\u00f3s, V.T. (eds.) Erd\u0151s Centennial, pp. 265\u2013287. Springer, Berlin (2013)"},{"key":"9650_CR21","volume-title":"Ramsey Theory","author":"RL Graham","year":"1991","unstructured":"Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory, 2nd edn. Wiley, Hoboken (1991)","edition":"2"},{"issue":"2","key":"9650_CR22","doi-asserted-by":"publisher","first-page":"481","DOI":"10.4007\/annals.2008.167.481","volume":"167","author":"B Green","year":"2008","unstructured":"Green, B., Tao, T.: The primes contain arbitrarily long arithmetic progressions. Ann. Math. 167(2), 481\u2013547 (2008)","journal-title":"Ann. Math."},{"key":"9650_CR23","unstructured":"Kreuzer, K.,\u00a0Eberl, M.: Van der Waerden\u2019s theorem. Archive of Formal Proofs (2021). https:\/\/isa-afp.org\/entries\/Van_der_Waerden.html"},{"issue":"3","key":"9650_CR24","doi-asserted-by":"publisher","first-page":"1551","DOI":"10.1090\/S0002-9947-2013-05820-5","volume":"366","author":"M Malliaris","year":"2014","unstructured":"Malliaris, M., Shelah, S.: Regularity lemmas for stable graphs. Trans. Am. Math. Soc. 366(3), 1551\u20131585 (2014)","journal-title":"Trans. Am. Math. Soc."},{"issue":"2","key":"9650_CR25","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1002\/rsa.20117","volume":"28","author":"B Nagle","year":"2006","unstructured":"Nagle, B., R\u00f6dl, V., Schacht, M.: The counting lemma for regular $$k$$-uniform hypergraphs. Random Struct. Algorithms 28(2), 113\u2013179 (2006)","journal-title":"Random Struct. Algorithms"},{"key":"9650_CR26","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C.,\u00a0Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer (2002). http:\/\/isabelle.in.tum.de\/dist\/Isabelle\/doc\/tutorial.pdf","DOI":"10.1007\/3-540-45949-9"},{"key":"9650_CR27","doi-asserted-by":"crossref","unstructured":"Noschinski, L.: A probabilistic proof of the girth-chromatic number theorem. Archive of Formal Proofs (2012). https:\/\/isa-afp.org\/entries\/Girth_Chromatic.html","DOI":"10.1007\/978-3-642-32347-8_27"},{"issue":"1","key":"9650_CR28","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/s11786-014-0183-z","volume":"9","author":"L Noschinski","year":"2015","unstructured":"Noschinski, L.: A graph library for Isabelle. Math. Comput. Sci. 9(1), 23\u201339 (2015)","journal-title":"Math. Comput. Sci."},{"issue":"2","key":"9650_CR29","first-page":"221","volume":"60","author":"M Raussen","year":"2013","unstructured":"Raussen, M., Skau, C.: Interview with Endre Szemer\u00e9di. Notices AMS 60(2), 221\u2013231 (2013)","journal-title":"Notices AMS"},{"issue":"1","key":"9650_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1002\/rsa.20017","volume":"25","author":"V R\u00f6dl","year":"2004","unstructured":"R\u00f6dl, V., Skokan, J.: Regularity lemma for $$k$$-uniform hypergraphs. Random Struct. Algorithms 25(1), 1\u201342 (2004)","journal-title":"Random Struct. Algorithms"},{"issue":"1","key":"9650_CR31","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1112\/jlms\/s1-28.1.104","volume":"s1\u201328","author":"KF Roth","year":"1953","unstructured":"Roth, K.F.: On certain sets of integers. J. Lond. Math. Soc. s1\u201328(1), 104\u2013109 (1953)","journal-title":"J. Lond. Math. Soc."},{"key":"9650_CR32","unstructured":"Szemer\u00e9di, E.: Regular partitions of graphs. Technical Report STAN-CS-75-489, Stanford University Computer Science Department (1975)"},{"key":"9650_CR33","doi-asserted-by":"publisher","first-page":"199","DOI":"10.4064\/aa-27-1-199-245","volume":"27","author":"E Szemer\u00e9di","year":"1975","unstructured":"Szemer\u00e9di, E.: On sets of integers containing $$k$$ elements in arithmetic progression. Acta Arith. 27, 199\u2013245 (1975)","journal-title":"Acta Arith."},{"issue":"1","key":"9650_CR34","first-page":"8","volume":"1","author":"T Tao","year":"2006","unstructured":"Tao, T.: Szemer\u00e9di\u2019s regularity lemma revisited. Contrib. Discret. Math. 1(1), 8\u201328 (2006)","journal-title":"Contrib. Discret. Math."},{"key":"9650_CR35","unstructured":"Zhao, Y.: Graph theory and additive combinatorics. (2017) https:\/\/yufeizhao.com\/gtac\/gtac17.pdf"},{"key":"9650_CR36","doi-asserted-by":"crossref","unstructured":"Zhao, Y.: Graph theory and additive combinatorics. (2022) https:\/\/yufeizhao.com\/gtacbook\/","DOI":"10.1017\/9781009310956"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09650-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09650-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09650-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,3]],"date-time":"2023-12-03T06:04:06Z","timestamp":1701583446000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09650-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,19]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["9650"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09650-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,12,19]]},"assertion":[{"value":"15 July 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 December 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178). Edmonds is jointly funded by the Cambridge Trust (Cambridge Australia Scholarship) and a Cambridge Department of Computer Science Premium Research Studentship. The authors have no financial or proprietary interests in any material discussed in this article. For the purpose of open access, the authors have applied a Creative Commons Attribution (CC BY) licence to any Author Accepted Manuscript version arising from this submission.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"2"}}