Zulip Chat Archive

Stream: graph theory

Topic: Intro to Graph Theory in Lean


Ayush Agrawal (Oct 18 2021 at 15:01):

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 (Oct 18 2021 at 15:13):

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 (Oct 18 2021 at 15:22):

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 (Oct 18 2021 at 15:37):

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

Ayush Agrawal (Oct 18 2021 at 15:49):

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

Kyle Miller (Oct 18 2021 at 15:51):

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 (Oct 18 2021 at 16:01):

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 (Oct 18 2021 at 16:07):

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

Ayush Agrawal (Oct 18 2021 at 20:05):

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 (Oct 18 2021 at 20:16):

@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 (Oct 18 2021 at 20:17):

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

Ayush Agrawal (Oct 18 2021 at 20:18):

and using the three definitions we have for the structure

Kyle Miller (Oct 18 2021 at 20:19):

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 (Oct 18 2021 at 20:19):

(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 (Oct 18 2021 at 20:20):

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


Last updated: Dec 20 2023 at 11:08 UTC