Turán's Graph Theorem

Nils Lauermann 📧

November 14, 2022


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