Flow networks

Stream: graph theory

[Aleksandar Milchev]

Hello! I am a new user and I would like to contribute to the library by implementing a proof for the Max-Flow Min-Cut theorem for flow networks. However, helpful people told me that there is no definition for flow networks. I was advised to use quivers. Is that the best way to approach the problem? If not, what other recommendation you would give me? Thank you!

[Julian Külshammer]

Last summer, @Justin Pearson and I supervised two students who started on formalising this theorem, but as far as I know didn't complete it. If you are interested, I could put you in contact with them.

[Vincent Beffara]

Last year I managed to prove Menger's theorem for simple_graph, which is related, but the API around paths was not easy to use (for type-theoretic reasons, like e.g. the statement that a path stopped on its first hitting point of a set was equal to another path did not want to type-check). So the code is really a mess ...

[Aleksandar Milchev]

Julian Külshammer said:

Last summer, Justin Pearson and I supervised two students who started on formalising this theorem, but as far as I know didn't complete it. If you are interested, I could put you in contact with them.

That will be great, thank you!