Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Szemerédi's Regularity Lemma


view this post on Zulip Email Gateway (Nov 07 2021 at 16:40):

From: Tobias Nipkow <nipkow@in.tum.de>
Szemerédi's Regularity Lemma
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Szemerédi's regularity lemma is a key result in the study of large graphs. It
asserts the existence an upper bound on the number of parts the vertices of a
graph need to be partitioned into such that the edges between the parts are
random in a certain sense. This bound depends only on the desired precision and
not on the graph itself, in the spirit of Ramsey's theorem. The formalisation
follows online course notes by Tim Gowers and Yufei Zhao.

https://www.isa-afp.org/entries/Szemeredi_Regularity.html

Enjoy!
smime.p7s


Last updated: Jul 15 2022 at 23:21 UTC