Max-Flow Min-Cut Theorem in Lean

Introduction:

This project strives to contribute to and is dependent on mathlib, the library of the Lean theorem prover. The aim for the file is to implement the Max-Flow Min-Cut theorem, stating that if a maximum flow exists in a flow network, then its value is equal to the capacity of the minimum cut in the same network. Introduction to the field and formal proof of the theorem can be found in this file.

References:

• The code is based on the first try to prove the theorem by Leo Okawa Ericson and Viggo Laakshoharju.
• The proof is based on the [Combinatorial Optimisation] (https://onlinelibrary.wiley.com/doi/book/10.1002/9781118033142) book by William J. Cook, William H. Cunningham, William R. Pulleyblank, Alexander Schrijver.
• A proof of the same theorem, implemented in mathlib4, can be followed here.