What to do

Stream: graph theory

[Yaël Dillies]

@Huỳnh Trần Khanh, you said you felt like doing graph theory. There's one thing that people aren't currently working on which would be nice to have. It's the counterexample to Hedetniemi's conjecture. Stuff has started at branch#hedetniemi and stalled because we need the fact that there exists graphs of arbitrary high girth and chromatic number (see https://en.wikipedia.org/wiki/Girth_(graph_theory)#Girth_and_graph_coloring). You probably won't make it to the end because it's a team-sized job, but if you manage to kick the can lower down the road it would be great already. Eg, I don't think we have a definition of girth currently, and I think that what Kyle is doing currently should be enough to provide the basics.

[Kyle Miller]

We should have enough in mathlib itself now to define girth, if you want to try @Huỳnh Trần Khanh.

There are two options for formalization: have the girth be a natural number, and if there are no cycles it's 0, or match the usual definition and have the girth take values in ℕ+, and if there are no cycles it's infinity. I'd probably do the second, but I wanted to float the first idea in case anyone thought it wouldn't cause any problems.

The hedetniemi branch uses ℕ+ https://github.com/leanprover-community/mathlib/blob/hedetniemi/src/graph_theory/girth.lean

For the API, I'd suggest having a girth_at_least predicate like in this branch, but maybe instead girth could be a noncomputable function that returns the girth (rather than it being a predicate like in the branch). This would parallel docs#simple_graph.colorable and docs#simple_graph.chromatic_number

[Kyle Miller]

Right now, the notion of a cycle is an oriented cycle with a basepoint. To introduce one, you say (u : V) (c : G.walk u u) (hc : c.is_cycle), and then you have c.length for the length of the cycle.

[Kyle Miller]

If you don't want to get into defining new things right now, a nice small and useful thing would be to show that cycles have length at least 3. I'm pretty sure I haven't proved that among the connectivity PRs. (I imagine the proof would be: do cases on c repeatedly until its length is 3, showing a contradiction for each case until then. docs#walk is an inductive type similar to list.) Maybe docs#simple_graph.walk.is_cycle_def is useful to rewrite the is_cycle hypothesis.

[Yakov Pechersky]

One can build a forgetful injection into docs#cycle and use that.