4
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • 4
    $\begingroup$ 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/… $\endgroup$
    – macbeth
    Jun 2 at 2:28
  • 1
    $\begingroup$ 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. $\endgroup$
    – macbeth
    Jun 2 at 16:50
  • 1
    $\begingroup$ 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. $\endgroup$
    – macbeth
    Jun 2 at 16:51
  • 1
    $\begingroup$ @macbeth Alternatively it sounds tedious to extract information from the matrix, but perhaps that's my inexperience talking. $\endgroup$
    – Alex Byard
    Jun 3 at 14:57
  • 1
    $\begingroup$ @macbeth I'll give them a question about it. $\endgroup$
    – Alex Byard
    Jun 3 at 14:58

1 Answer 1

Reset to default
3
$\begingroup$

I guess it would be pretty fun and pretty efficient to implement a Graph library on top of AC-sets following AlgebraicRewriting.jl's lead. Lots of work though... But might be possible to leverage MathLib. 😄

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ I’d be interested - could we work on this together? $\endgroup$
    – Julius H.
    Jun 9 at 14:38
  • 2
    $\begingroup$ @hmltn I don't really understand Category Theory behind AC-sets and Algebraic Rewriting, and I'm not familiar with Mathlib, thus I'm of little help. :) Besides, I won't have free time at least until August. I'd advise against waiting for me before starting the project. :) $\endgroup$
    – Alex Chichigin
    Jun 10 at 9:42
  • 1
    $\begingroup$ Don't count me out! @hmltn I'd like to work on this too $\endgroup$
    – Alex Byard
    Jun 11 at 1:24
  • 1
    $\begingroup$ @AlexByard Please contact me at my email [email protected] or, I would prefer, join me on Discord, where I collaborate with ppl: discord.gg/rhVtxdJA , or any channels on my SE profile like Twitter or Patreon. I am ready to begin work, with you. Thank you. $\endgroup$
    – Julius H.
    Jun 11 at 8:36
  • 1
    $\begingroup$ @hmltn I joined the discord under the name K10. Send me a message and we can start to work! $\endgroup$
    – Alex Byard
    Jun 11 at 17:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.