Visualization of mathlib dependency graph on a theorem level

Stream: mathlib4

[Oliver Dressler]

I have just uploaded a theorem-level dependency graph visualization of mathlib v4.15.0-rc1:

oli.show/leanstructure

Would love some feedback on how to make this more useful!

[Notification Bot]

This topic was moved here from #mathlib4 > Visualization of theorem dependency graph by Oliver Dressler.

[Jireh Loreaux]

that's fun! Can you explain what this means:

The total number of displayed nodes (500) and the number of neighbors are limited by random sampling.

What are you sampling randomly? And what is a neighbor? I would have expected children (or parents, depending on how you think about it).

[Jireh Loreaux]

It would also be nice if the search query were included in the url, for ease of sharing (even if that share is nondeterministic in certain situations).

[Oliver Dressler]

Jireh Loreaux said:

that's fun! Can you explain what this means:

The total number of displayed nodes (500) and the number of neighbors are limited by random sampling.

What are you sampling randomly? And what is a neighbor? I would have expected children (or parents, depending on how you think about it).

This random sampling is mainly not to overload the visualization. The limits are:

• 500 total nodes
• Max 100 neighbors of the initial node
• Max 50 neighbors of all subsequent nodes

Neighbors is just because they can be either child/parent depending if you look for dependencies or foundation; Click node, "foundation for x" will look "up" the dependency tree.

[Oliver Dressler]

Jireh Loreaux said:

It would also be nice if the search query were included in the url, for ease of sharing (even if that share is nondeterministic in certain situations).

Thats a great point. I'll look into including the search term/current node in the URL.

[Mario Carneiro]

you could put the seed in the url too to avoid the nondeterminism part

[Oliver Dressler]

Mario Carneiro said:

you could put the seed in the url too to avoid the nondeterminism part

Makes sense. The seed can be relatively short, and is only required in some cases.
Some more info is anyways required. Namely the direction of the bfs.

Graph simplifications (double-clicking nodes) are ignored.

URLs are now shareable, like:
https://oli.show/leanstructure/#0,0,Nat.exists_infinite_primes

[Edward van de Meent]

i like this one, it clearly shows how versatile docs#rfl is

[Kevin Buzzard]

Screenshot from 2024-12-11 22-03-40.png

[Oliver Dressler]

Yes, docs#rfl is the most used node (by 21053 theorems). This is just 100 of them! You can change the seed for the sampling either directly in the url (first int after the #) or by clicking the node and then clicking the "Foundation For 21053" button (random seed).

Just out of curiousity: PhragmenLindelof.horizontal_strip is the node which uses the most direct dependencies (114).