# Zulip Chat Archive

## Stream: graph theory

### Topic: Flow networks

#### Aleksandar Milchev (Dec 15 2022 at 14:34):

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 (Dec 15 2022 at 15:48):

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 (Dec 15 2022 at 16:47):

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 (Dec 15 2022 at 19:12):

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!

Last updated: Dec 20 2023 at 11:08 UTC