### 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 $\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.### License

### Topics

### Related publications

- Aigner, M., & Ziegler, G. M. (2018). Turán’s graph theorem. Proofs from THE BOOK, 285–289. https://doi.org/10.1007/978-3-662-57265-8_41