Zulip Chat Archive

Stream: new members

Topic: Mathlib Graph

ccn (Jan 09 2022 at 17:34):

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 (Jan 09 2022 at 17:37):

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 (Jan 09 2022 at 17:37):

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 (Jan 09 2022 at 17:39):

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

Alex J. Best (Jan 09 2022 at 17:51):

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

Last updated: Dec 20 2023 at 11:08 UTC