Formalizing Kirchhoff's theorem

Stream: mathlib4

[Brian Nugent]

I would like to work on formalizing Kirchhoff's theorem for simple graphs. Is anyone actively working on graph theory for mathlib?

[Snir Broshi]

Brian Nugent said:

Is anyone actively working on graph theory for mathlib?

Yes

[Snir Broshi]

Sounds great! What's the plan?

[Brian Nugent]

I was planning on following the inductive proof given here to avoid the Cauchy Binet formula. I was going to start with edge contraction since that's a useful concept for other things as well.

[Snir Broshi]

tbh I'm not sure edge-contraction will be in Mathlib before #33466 and the corresponding SimpleGraph refactor. I suggest reading the discussion from December 9th here #graph theory > What kind of graphs are in Mathlib already? @ 💬

[Snir Broshi]

But if you have a good plan for edge-contraction it's worth a shot

[Brian Nugent]

I was planning on avoiding Quotient and instead defining it as a graph on a subset of V. I can see why it would be good to wait for the refactor, thank you for showing me this!

[Brian Nugent]

Is it reasonable to work off of it as a dependency or is that a bad idea since it will be changing?

[Snir Broshi]

The PR I linked is for Digraph, we'd need a similar one for SimpleGraph first.
OTOH maybe you can prove Kirchhoff's theorem for digraphs?

[Yaël Dillies]

We have edge deletion and contraction both in ProofBench (secret) and in FormalConjectures (in a PR). Working hard on bringing them to mathlib

[Brian Nugent]

Ok, seems like it might be best if I just hold off for a bit then

[Brian Nugent]

On the other hand, this is the first I'm hearing of the FormalConjectures repo, I think I'll give one of those a go!