graphs

Stream: Lean for teaching

[Alexandre Rademaker]

Does anyone know about any attempt to formalize in Lean graphs ? I am looking for results generally presented in a discrete math course

[Bryan Gin-ge Chen]

I don't think that many results from such a course have yet been formalized (though I'd love to be proven wrong). There are a few attempts you can find in Zulip if you search for "graph" or "graphs", e.g. this recent thread, this slightly older one and this even older one. There's also this gist by @Jeremy Avigad (with accompanying comments here).

[Kevin Buzzard]

This has come up before, and the general problem seems to be that there are ten different kinds of formalised things that are informally all called "graphs".

[Johan Commelin]

@Kevin Buzzard You mean "formalisable" not "formalised", right?

[Johan Commelin]

As in... there aren't 10 Lean files at the moment.

[Kevin Buzzard]

Yes. I mean simply that the edges may or may not be directed, multiple edges may be allowed and so on.

[Alexandre Rademaker]

Yes @Kevin Buzzard , many different ways. I am trying to find simple examples for my next course on discrete math. This semester I didn’t cover graphs

[Kevin Buzzard]

I have been asked to give a one day Lean workshop at a combinatorics conference for PhD students in April and I would be very interested in any work on formalising any kind of graph theory

[Bhavik Mehta]

I have been asked to give a one day Lean workshop at a combinatorics conference for PhD students in April and I would be very interested in any work on formalising any kind of graph theory

Similarly

[Kevin Buzzard]

In my experience, a good way of starting with something like this is deciding on a goal, e.g. every tree on n+1 vertices has n edges, or every graph is uniquely a disjoint union of connected subgraphs, and then trying to prove this and figuring out what else you should have proved first along the way. Ideally this should turn into a mathlib PR. I would stay well away from planar graphs right now as there will be several competing formalised definitions and they'll be hard to work with. I don't know enough about the area to know a nice healthy list of basic theorems but one should fix a definition of graph (e.g. undirected, at most one edge between two vertices, no edge from a vertex to itself?) and then develop a basic theory, enough to make it usable for teaching.