Email Gateway (Jan 03 2022 at 09:17): Email Gateway (Jan 03 2022 at 09:17):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
We have our first two new AFP entries in 2022:
Roth's Theorem on Arithmetic Progressions
by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson
We formalise a proof of Roth's Theorem on Arithmetic Progressions, a major result in
additive combinatorics on the existence of 3-term arithmetic progressions in subsets of
natural numbers. To this end, we follow a proof using graph regularity. We employ our
recent formalisation of Szemerédi's Regularity Lemma, a major result in extremal graph
theory, which we use here to prove the Triangle Counting Lemma and the Triangle Removal
Lemma. Our sources are Yufei Zhao's MIT lecture notes "Graph Theory and Additive
Combinatorics" (revised version here) and W.T. Gowers's Cambridge lecture notes "Topics in
Combinatorics". We also refer to the University of Georgia notes by Stephanie Bell and
Will Grodzicki, "Using Szemerédi's Regularity Lemma to Prove Roth's Theorem".
https://www.isa-afp.org/entries/Roth_Arithmetic_Progressions.html
Gale-Shapley Algorithm
by Tobias Nipkow
This is a stepwise refinement and proof of the Gale-Shapley stable matching (or marriage)
algorithm down to executable code. Both a purely functional implementation based on lists
and a functional implementation based on efficient arrays (provided by the Collections
Framework in the AFP) are developed. The latter implementation runs in time O(n2) where n
is the cardinality of the two sets to be matched.
https://www.isa-afp.org/entries/Gale_Shapley.html
Andreas
Last updated: Apr 20 2024 at 04:19 UTC