# Menger's Theorem

 Title: Menger's Theorem Author: Christoph Dittmann Submission date: 2017-02-26 Abstract: We present a formalization of Menger's Theorem for directed and undirected graphs in Isabelle/HOL. This well-known result shows that if two non-adjacent distinct vertices u, v in a directed graph have no separator smaller than n, then there exist n internally vertex-disjoint paths from u to v. The version for undirected graphs follows immediately because undirected graphs are a special case of directed graphs. BibTeX: @article{Menger-AFP, author = {Christoph Dittmann}, title = {Menger's Theorem}, journal = {Archive of Formal Proofs}, month = feb, year = 2017, note = {\url{http://isa-afp.org/entries/Menger.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.