Graph theory project

Stream: new members

[Iván Renison]

Hello, I'm Iván Renison, I'm taking a course in formalization in the National University of Cordoba, and for the course I have to formalize something.
I'm thinking in formalizing something about graph theory, maybe graph coloring. One option that I have in mind is Brooks' theorem
Do you have some suggestions?

[Kevin Buzzard]

That theorem will certainly be a challenge for a beginner! I tell students that it's fine to aim high and then not get there and sorry some intermediate results. The only downside to this is that occasionally students aim high, get absolutely nowhere, and then sorry a statement which is just as hard as what they're trying to prove in the first place

[Yaël Dillies]

I personally think that's a reasonable theorem, but you'll have to give some thought so as to which proof you'll formalise. What proof do you know?

[Iván Renison]

The proof that I know for irregular graphs uses greedy colouring, and for regular graph shows a way of modifying a greedy colouring (dividing in a lot of cases and using Kempe chains) to make it have at most Δ colours

[Martin Dvořák]

Would it get significantly easier if you just wanted to prove that every graph is (Δ+1)-colorable?

[Yaël Dillies]

Yeah. Color greedily.

[Martin Dvořák]

Yeah. This might be a good target for a school project, I think.

[Iván Renison]

And do you have some other suggestions of theorems?
I have until the end of November in time, so it can be something relatively long, and I think that it would be good if it has lots of intermediate results

[Yaël Dillies]

A fun one would be Dirac. I've thought about it and I decided it would make for a good project involving paths, cycles, Posa rotations...

[Iván Renison]

According to Wikipedia:

Dirac's theorem may refer to:
• Dirac's theorem on Hamiltonian cycles, the statement that an n-vertex graph in which each vertex has degree at least n/2 must have a Hamiltonian cycle
• Dirac's theorem on chordal graphs, the characterization of chordal graphs as graphs in which all minimal separators are cliques
• Dirac's theorem on cycles in k-connected graphs, the result that for every set of k vertices in a k-vertex-connected graph there exists a cycle that passes through all the vertices in the set

Are you referring to one of those in particular?

[Mauricio Collares]

The first one

[Iván Renison]

Ok, it looks good, thank you

[Linus Sommer]

@Bhavik Mehta @Rishi Mehta @Abhiruk Lahiri and I already started working on this. We will finish the definitions soon.

[Iván Renison]

Are you working on Dirac's theorem?

[Rishi Mehta]

We were, but as a first step we're adding the definitions of Hamiltonian paths and cycles, and some basic lemmas about them. (our branch)

[Iván Renison]

Okey, I will continue with the idea of doing the project in Dirac's theorem, and if I can I will use your definitions and basic lemmas

[Iván Renison]

Also, if I end up having extra time I have Ore's theorem in mind

[Iván Renison]

Do you know when you are going to merge your branch?

[Iván Renison]

Hello @Linus Sommer and @Rishi Mehta, now I'm ready to start working on Dirac's theorem, if you are not going to prove it can I have access to your branch and work there?
Mi github username is IvanRenison
Or I should do it in my own branch on top of yours?

[Linus Sommer]

Hello Ivan,
I am not sure about that. Theoretically our branch is ready for merging unless there are any complaints from the maintainers. @Bhavik Mehta what do you say? Oh I guess we forgot to add the tag awaiting-review. Maybe someone can review it and you can start working on a copy of our branch for now?

[Kevin Buzzard]

@Linus Sommer if a PR is not on the #queue then essentially nobody will notice it.

[Iván Renison]

Ok, I see that you branch is in PR, but, I see that you have the Dirac theorem stated with a sorry (as I see, in a commit you deleted it, but two commits after you add it again)

[Bhavik Mehta]

The branch should now be ready for review - probably the easiest is to make a new branch on top of this one (eg by just copying over the relevant file)