Email Gateway (Dec 01 2022 at 13:35): Email Gateway (Dec 01 2022 at 13:35):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’d like to announce a new AFP-entry.
Turán's Graph Theorem
by Nils Lauermann
Abstract:
Turán's Graph Theorem states that any undirected, simple graph with n vertices
that does not contain a p-clique, contains at most (1 - 1/(p-1)) * n^2 / 2
edges. The theorem is an important result in graph theory and the foundation of
the field of extremal graph theory. The formalisation follows Aigner and
Ziegler's presentation in Proofs from THE BOOK of Turán's initial proof. Besides
a direct adaptation of the textbook proof, a simplified, second proof is
presented which decreases the size of the formalised proof significantly.
https://www.isa-afp.org/entries/Turans_Graph_Theorem.html
Enjoy,
René
Last updated: Jan 04 2025 at 20:18 UTC