edge connectivity

Stream: new members

[Abhinav N]

Hello , we are thinking of working in edge connectivity.Is there any starting point for this and are there any specifications to follow?

[Notification Bot]

A message was moved here from #new members > extrema, R^n by Kevin Buzzard.

[Jakub Nowak]

We have a definition in mathlib and a few basic lemmas, but there's not much more. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.html

@Yaël Dillies might share more about plans for that maybe?

Btw "Youheng Luo" is listed as an author, but he's not here on Zulip under that name. I think it might be @Terence Prime? Sorry, if I was wrong. Could you update you're name either here on Zulip, or in that mathlib file?

[Snir Broshi]

What are you planning to do in edge connectivity?

[Yaël Dillies]

I have a proof of a recent graph theory result in a secret repo, and the proof crucially uses the decomposition of a specific graph into its two-connected components. My plan is to upstream all the prerequisites to the proof, but not the proof itself which must stay secret.

[Jakub Nowak]

If you want the proof to stay secret, but not the result, you can post non-interactive zero-knowledge proof. :slight_smile: (joking)

[Abhinav N]

Kindly suggest some topics in the area of vertex/edge connectivity that are needs to be worked on.

[Ioannis Tsiokos]

hi everybody! my background is in comp sci and biochem, and I am trying to formalize an emergence calculus framework :-D

[Snir Broshi]

Abhinav N said:

Kindly suggest some topics in the area of vertex/edge connectivity that are needs to be worked on.

You posted that you want to work on edge-connectivity, so I thought you had something in mind that needs doing. If not, then why did you choose this super specific area? What's your goal? Is it graph theory in general? Help us help you.

[Snir Broshi]

If you're looking for graph-theory stuff to do, check out #new members > Looking for a first project (Graph Theory / Combinatorics) @ 💬 and update here if you're working on any of these