working with explicit graphs

Stream: graph theory

[Andrea Nardi]

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]

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]

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]

Oh great, thanks!

[kbridge]

for mathlib4, use https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Konigsberg.lean