A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory

Aharoni et al. (J Combinat Theory, Ser B 101:1-17, 2010) proved the max-flow min-cut theorem for countable networks, namely that in every countable network with finite edge capacities, there exists a flow and a cut such that the flow saturates all outgoing edges of the cut and is zero on all incoming edges. In this paper, we formalize their proof in Isabelle/HOL and thereby identify and fix several problems with their proof. We also provide a simpler proof for networks where the total outgoing capacity of all vertices other than the source and the sink is finite. This proof is based on the max-flow min-cut theorem for finite networks. As a use case, we formalize a characterization theorem for relation lifting on discrete probability distributions and two of its applications.

Automated summary

This paper formalizes and fixes Aharoni et al.'s proof of the max-flow min-cut theorem in Isabelle/HOL. It also provides a simpler proof for a sub-class of networks and applies it to relation lifting on discrete probability distributions.