Menger's Theorem

Christoph Dittmann 📧

February 26, 2017

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


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.


BSD License


Session Menger