### 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

BSD License

### Topics

- Mathematics/Graph theory

### 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

### Session Turans_Graph_Theorem

- Turan

### Depends on

- A Probabilistic Proof of the Girth-Chromatic Number Theorem
- Properties of Random Graphs – Subgraph Containment

### Auto-related entries

- The Balog–Szemerédi–Gowers Theorem
- Roth’s Theorem on Arithmetic Progressions
- Selected Problems from the International Mathematical Olympiad 2019

## Cite

×

Turans_Graph_Theorem-AFP

    @article{Turans_Graph_Theorem-AFP,
      author  = {Nils Lauermann},
      title   = {Turán's Graph Theorem},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Turans_Graph_Theorem.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Dec 1, 2022 : Isabelle2022