Zulip Chat Archive

I also have a student who's working towards the adjacency matrix formula for counting walks. Walks seem easier than paths to deal with, but he's also just starting learning Lean, so it'll take some time.

Alena Gusakov (Dec 02 2020 at 22:11):

Chromatic/Tutte polynomials:

Whitney Broken Circuit Theorem: Definition of the chromatic polynomial and Stirling numbers (!!), prove that the chromatic polynomial satisfies the deletion-contraction recurrence, prove that Stirling numbers allow for a “change of basis” from the standard basis to the basis of falling factorials (associated with two different ways of counting), and prove that the coefficients of the chromatic polynomial correspond to various properties of the graph. (This is where quotient types in Lean become useful - one concept associated with the chromatic polynomial is chromatic equivalence)
Tutte polynomial: Define, demonstrate that it is a generalization of the chromatic polynomial. Specialize the Tutte polynomial to other useful polynomials, such as the Reliability Polynomial (used for networks) and the Jones polynomial (used in knot theory). Formalize a proof of the Universality Property of the Tutte polynomial, which states that any graph invariant that is multiplicative on disjoint unions and one-point joins of graphs and that satisfies the deletion-contraction recurrence must be an evaluation of the Tutte polynomial.

Aaron Anderson (Dec 02 2020 at 22:13):

It'd be nice to prove some things about chromatic numbers. Some results there will fall out of the chromatic polynomial, but some results will need a different approach. Many of the obvious candidates (5-color theorem) require a definition of planar graph, which I expect will be tricky.

Kyle Miller (Dec 02 2020 at 22:14):

For planar graphs, what I had in mind was defining combinatorial maps, and then say a planar graph is the skeleton of a genus-0 combinatorial map. I have code for them somewhere (including duals and such).

Kyle Miller (Dec 02 2020 at 22:15):

You can get the 5-color theorem using a certain exceptional relation that arises from the chromatic polynomial at n=5, but you don't need the polynomial itself for that.

Aaron Anderson (Dec 02 2020 at 22:16):

One thing that's definitely easy: The Handshake Lemma (the sum of the degrees is twice the number of edges). I know Kyle has proved this somewhere, but I'd kind of like to see a proof using incidence matrices.

Kyle Miller (Dec 02 2020 at 22:18):

The degree-sum formula is in simple_graphs2 using a combinatorial argument (that still has room for improvement, iirc). (I think the Handshake lemma is specifically the degree-sum formula mod 2?)

Kyle Miller (Dec 02 2020 at 22:25):

A comment about Tutte polynomials: they're more naturally defined for multigraphs, so those need development. For one version of it, we need to be able to sum over spanning subgraphs of the monomials $u^Ev^c$ where $E$ is the number of edges and $c$ is the number of connected components of the subgraph. If you want to do something like the dichromatic polynomial directly, then you'll need to be able to calculate the nullity of a subgraph, which is the rank of the first homology, i.e. the nullity of a signed incidence matrix.

Bryan Gin-ge Chen (Dec 02 2020 at 22:25):

Tutte polynomials should probably be done at the level of matroids, but I'm not sure if we should wait for those.

Kyle Miller (Dec 02 2020 at 22:30):

@Bryan Gin-ge Chen I think there are some reasons to do Tutte polynomials for graphs directly. The chromatic polynomial, for example, isn't an invariant of the graphic matroid unless the graph is connected, I think.

Aaron Anderson (Dec 02 2020 at 22:31):

Stuff that feels like it should be easy, but probably needs some more basic definitions: the number of edges in an acyclic graph is the number of vertices minus the number of components

Kyle Miller (Dec 02 2020 at 22:32):

There are lots of manipulations you can do if you just define it to be $Q_G(u,v)=\sum_{S\subseteq G}u^{b_0(S)}v^{b_1(S)}$ , where the sum is over spanning subgraphs, and $b_i(S)=\operatorname{rk}H_i(S)$ is the Betti number. Euler characteristic is a very useful identity for manipulations: $\lvert V(G)\rvert-\lvert E(G)\rvert=b_0(G)-b_1(G)$ .

Kyle Miller (Dec 02 2020 at 22:34):

Aaron Anderson said:

Stuff that feels like it should be easy, but probably needs some more basic definitions: the number of edges in an acyclic graph is the number of vertices minus the number of components

If we prove the Euler characteristic formula above and that a graph is acyclic iff $b_1(G)=0$ , then we'd get this.

Kyle Miller (Dec 02 2020 at 22:35):

(We'd also need that $b_0(G)$ is the number of components.)

Bryan Gin-ge Chen (Dec 02 2020 at 22:43):

~~Connected components will require paths too. Is there a plan for paths yet?~~ (whoops, I'd better review my definitions...)

Aaron Anderson (Dec 02 2020 at 22:46):

Bryan Gin-ge Chen said:

Connected components will require paths too. Is there a plan for paths yet?

They will not require paths. They'll either need walks (like paths but without the troublesome injectivity assumption) or just a connectedness relation which is the transitive closure of the adjacency relation.

Alena Gusakov (Dec 02 2020 at 22:51):

Oh also, I want to do vertex/edge connectivity at some point and Menger's theorem

Kyle Miller (Dec 02 2020 at 22:51):

simple_graphs2 has some code for walks in combinatorics/simple_graph/walks.lean, but it's definitely a draft.

Kyle Miller (Dec 02 2020 at 22:55):

Bryan Gin-ge Chen said:

Connected components will require paths too. Is there a plan for paths yet?

https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph/walks.lean#L895

There are also some sorrys for showing the two definitions Aaron gave are equivalent, as well as that path connectivity and walk connectivity are the same relation.

Alena Gusakov (Dec 02 2020 at 23:31):

path connectivity and walk connectivity are the same relation.

I spent so much time trying to prove this jesus christ

Bhavik Mehta (Dec 03 2020 at 12:51):

I'd like to get finite and infinite Ramsey in at some point, but my inclination is that it doesn't necessarily need to be considered here: I found it most convenient for infinite Ramsey to just consider colourings finset N -> K (satisfying certain conditions), then the application to an arbitrary countable simple_graph just involves shifting it to be a graph on N and checking those conditions at r=2 (and for uncountable graphs just picking a countable bit and doing the same)

Kyle Miller (Dec 06 2020 at 13:38):

Aaron Anderson said:

The Handshake Lemma (the sum of the degrees is twice the number of edges).

I've put a combinatorial proof at https://github.com/leanprover-community/mathlib/blob/degree-sum/src/combinatorics/simple_graph/handshake.lean along with some sorryied corollaries, if anyone wants to finish it up and create a PR. This branch is based on #5191, so it will need to be rebased once that is merged.

The argument is basically equivalent to the proof that in an undirected incidence matrix, the row sums are degrees and column sums are all 2. It just introduces a combinatorial object, called a dart, with one per 1 in the matrix.

Aaron Anderson (Dec 06 2020 at 23:42):

The Matrix Tree Theorem would be good.

Last updated: Dec 20 2023 at 11:08 UTC