Turán's Graph Theorem

Nils Lauermann 📧

November 14, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Turán's Graph Theorem states that any undirected, simple graph with $n$ vertices that does not contain a $p$-clique, contains at most $\left( 1 - \frac{1}{p-1} \right) \frac{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.


BSD License


Related publications

Session Turans_Graph_Theorem