Stream: Lean for teaching

Topic: graphs

Alexandre Rademaker (Oct 22 2019 at 23:21):

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 (Oct 22 2019 at 23:32):

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 (Oct 23 2019 at 06:30):

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 (Oct 23 2019 at 06:44):

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

Johan Commelin (Oct 23 2019 at 06:45):

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

Kevin Buzzard (Oct 23 2019 at 06:45):

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

Alexandre Rademaker (Nov 22 2019 at 02:05):

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 (Nov 22 2019 at 07:00):

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 (Nov 22 2019 at 10:19):

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 (Nov 22 2019 at 12:02):

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.

Last updated: Dec 20 2023 at 11:08 UTC