Zulip Chat Archive

Stream: graph theory

Topic: working with explicit graphs

Andrea Nardi (Nov 06 2022 at 15:25):

I am new to Lean,

I wanted to warm myself into graph theory proving by proving simple properties on graphs that I explicitaly made. How can I, in code, make a graph with an e.g. edge list?

Kyle Miller (Nov 06 2022 at 15:29):

Here's an example of an explicit graph in the mathlib archive: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/54_konigsberg.lean

Some of the additional definitions (like for vertex degrees) are to help Lean in some arguments by caching results.

Kyle Miller (Nov 06 2022 at 15:31):

I can't find it immediately, but there's another example in this graph theory stream for creating a simple graph using a different representation. There's also an open PR for creating graphs from an edge set.

Andrea Nardi (Nov 06 2022 at 15:41):

Oh great, thanks!

Last updated: Dec 20 2023 at 11:08 UTC