Menger's theorem

Stream: new members

[Abhinav N]

Hello, we have set up lean 4 and are thinking of contributing to the graph theory section specifically regarding proving menger's theorem. We are following Douglas .B. West as a reference, defining and proving in the order of reference. What are the specific coding standards to follow and is there anything we need to be aware of?

[Snir Broshi]

Welcome :wave:
If you're new to the community I'd recommend first contributing smaller scale stuff, it's easier to get a big PR merged if you're already versed in Mathlib's conventions.
I'd love to see Menger's theorem in Mathlib, here are some pointers: Edge connectivity is in file#Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity, and we don't yet have vertex connectivity (#33355). In #34028 the author also mentioned they'd like to work on Menger's.
As for coding standards, see #style and #naming.

[Abhinav N]

Thanks @Snir Broshi for the advice. Should we start by providing any missing documentation or proving some smaller theorems like every edge is a cut-edge in a tree? Do you have any recommendations?

[Rida Hamadani]

@Vincent Beffara proved Menger's theorem in lean3: https://github.com/vbeffara/lean/tree/main/src/graph_theory
I'm not sure how portable it is (probably not very, due to complications related to how to define minors in mathlib).

[Thomas Waring]

Abhinav N said:

... every edge is a cut-edge in a tree?

Smaller results are a great idea, though this one already exists (if I have interpreted "cut-edge" correctly) as docs#SimpleGraph.isAcyclic_iff_forall_edge_isBridge

[Snir Broshi]

Abhinav N said:

Do you have any recommendations?

Check out #new members > Looking for a first project (Graph Theory / Combinatorics) @ 💬