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

Chelsea Edmonds, Angeliki Koutsoukou Argyraki, Lawrence C. Paulson. Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. Journal of Automated Reasoning, 67(1):2, 2023. [doi]

Authors

Chelsea Edmonds

This author has not been identified. Look up 'Chelsea Edmonds' in Google

Angeliki Koutsoukou Argyraki

This author has not been identified. Look up 'Angeliki Koutsoukou Argyraki' in Google

Lawrence C. Paulson

This author has not been identified. Look up 'Lawrence C. Paulson' in Google