# Graph Theory in Lean

I can't find an implementation of graph theory in Mathlib. Am I overlooking the file, or is it particularly difficult to do this, or has no one been interested in taking this on yet?

If it hasn't been done, what would be a good way to model the vertices of a graph? This seems to be the first crucial task, as once this is complete edges are easy to define, as are weights, vertex neighbors, etc. My general vision is that we should define types Vertex and have VertexSet be a set of types Vertex. Then Edge could be a 2-element set of types Vertex belonging to a particular VertexSet, and EdgeSet be a set of types Edge. Graph could extend typeclasses VertexSet and EdgeSet, I think.

But perhaps this is too difficult. Could Graph just be a typeclass with fields including a vertex set of Nats, hence abusing the order of Nat to order vertices, and an edge set of 2-element sets of vertices? I'd appreciate any intuition on this matter from more-experienced engineers. I'm certain I'm overlooking something.

I'm also thinking about how to define Graph such that it can be extended to Digraph, WeightedGraph, etc. Adding weights could be an extension of Graph to include a w : E -> Real, where E is the edge set, as a new field. This would make it simple to call the weights, as well. How would we extend Graph to Digraph, which requires us to tag vertices in edges with head and tail somehow? I've considered adding functions head and tail mapping the edge set to the vertex set, but is there a way to require that these functions take values in the two vertices associated with the edge, or is this even necessary? Another idea would be that Digraph doesn't even need to extend Graph at all, and we could define it so that it's edge set is a set of pairs of vertices, so that we can call them separately. I'd also appreciate help thinking about this.

• I'll let others give feedback on your proposed implementation (it's certainly a good exercise to write one yourself), but here is the main implementation which you had trouble finding: leanprover-community.github.io/mathlib4_docs/Mathlib/… Jun 2 at 2:28
• Not in mathlib (as far as I know), probably partly because in any given application it's easier to use the trick of identifying with a matrix of booleans rather than to get sidetracked into developing a full theory. Jun 2 at 16:50
• But coincidentally I remember Alex Best and Peter Nelson discussing an API for digraphs just last week -- you could ask them about it on the Lean Zulip if you are interested. Jun 2 at 16:51
• @macbeth Alternatively it sounds tedious to extract information from the matrix, but perhaps that's my inexperience talking. Jun 3 at 14:57
• @macbeth I'll give them a question about it. Jun 3 at 14:58