Intro to Graph Theory in Lean

Stream: graph theory

[Ayush Agrawal]

Hi guys! Can someone recommend some resources to start theorem proving in graph theory in Lean. Some basic topics like defining the graph and simple theorems related to that, some tactics made for graphs etc.

[Kyle Miller]

I know @Barrie Cooper made a game for multigraphs here https://barriecooper.github.io/html/index.html

I'm not aware of any pre-written resources about learning Lean graph theory yet -- there really isn't that much of it. You can read the source code for docs#simple_graph, which is all in this directory, starting with basic.lean (just ignore . obviously if you're not familiar with it). There's also the friendship theorem as well as a few things in the PR queue, especially incidence matrices and paths/connectivity.

If there's some theorem you might be interested in formalizing, you can mention it here in the #graph theory stream and we can help plan it out.

[Kyle Miller]

There are definitely no graph theory specific tactics right now. (Maybe the closest, which is a stretch, is in #8737 when I tried to prove there was no Eulerian trail in the seven bridges of Konigsberg problem using dec_trivial, but it fails to work for a mysterious reason.)

[Ayush Agrawal]

Thanks @Kyle Miller . I'll look into these and get back!

[Ayush Agrawal]

Do u also have solutions for this game @Kyle Miller ?

[Kyle Miller]

I don't (and I've only read through its source code before -- I haven't tried it myself).

Note that it's about multigraphs, but mathlib only has simple graphs right now.

[Yaël Dillies]

Btw Kyle what's the status of #8737? I would love to help out but I'm already quite taken with SRL and the tripos.

[Kyle Miller]

@Yaël Dillies The status is that I've got some deadlines I need to meet for non-Lean things :sad:

[Ayush Agrawal]

It would be great if u could provide a snippet of how one would initialise a simple graph (eg a triangle ) using a simple_graph structure. It might make things more clearer for me regarding Lean also :)

[Kyle Miller]

@Ayush Agrawal A triangle happens to be docs#complete_graph given a type with three terms, for example complete_graph (fin 3) will do.

[Ayush Agrawal]

Nice! I was asking for some very trivial graph that could be formed using simple_graph structure

[Ayush Agrawal]

and using the three definitions we have for the structure

[Kyle Miller]

complete_graph defines a graph using the structure. It's able to skip sym and loopless because the tidy tactic is able to automatically fill in those proofs.

[Kyle Miller]

(This is the function of . obviously in the structure definition. It tells Lean to try the tidy tactic if that field is missing.)

[Kyle Miller]

You might also take a look at this topic which has some concrete simple graphs