Mathlib Graph

Stream: new members

[ccn]

Hello I am wondering if anyone has tried this out yet.

We make a dependency graph of mathlib, so an individual node would represent some sort of knowledge = lemma, theorem, def, etc... and then it has some attributes about it, like the main statement, the other knowledge it uses in it's proof or definitions that it uses.

There could also be structure nodes where the directory that it lives (in mathlib) would have a node representing it, so you could have something like Mathlib -> linear_algebra (structure) -> set.finrank (knowledge)

If we had that graph, then I think it would be a cool way to visualize everything because we look at some knowledge and trace it back through the tree until we get to the axioms, so you could see the path that we took to prove it.

I know that lean is a programming language, not just a theorem prover so maybe we could make this graph in lean?

[Alex J. Best]

People have definitely tried this, its quite hard to get something reasonable on the scale of mathlib, because it is so huge. But the authors of the Lean perfectoid project made a nice visualization using this sort of idea, check out https://leanprover-community.github.io/lean-perfectoid-spaces/

[Henrik Böving]

There does also exisit a mathlib import graph over here https://eric-wieser.github.io/mathlib-import-graph/ which isn't quite what you are talking about but gets rather close to it.

[ccn]

Thanks for the links, I'll try to look at the source code and see how it's done!

[Alex J. Best]

I think the tool used was https://github.com/leanprover-community/leancrawler