← Feed
@MartinEscardo@mathstodon.xyz
Post #2181927
2026-05-04 23:23 UTC
So I've learned a lot about a little of TypeTopology, by exploring its graph, in the last few days.
It is so interesting to see how things depend or not depend on each other, and what we consider in practice to be "the foundation of everything else".
One thing I have learned in my experiments this weekend is that its *chosen* module graph differs considerably from the actual dependencies of the functions/definitions within the various modules, which is a completely different graph.
And I suspect the same happens in unformalized mathematics as recorded in the literature. We organize things by mathematical subjects, rather than logical dependencies (except if you are Bourbaki, but, even then, I am not completely sure).
It was painful to explore this systematically, by the lack of tools I could find, even with your help here, and there is a lot more work to be done, but I am really interested in learning how mathematical ideas connect to each other "in practice and foundationally", from an experimental point of view, given the mathematics recorded in various repositories, including TypeTopology.
Replies (3)
-
@MartinEscardo@mathstodon.xyz is this what you meant by logical vs. genetic order?
Open ##2599023
-
@MartinEscardo@mathstodon.xyz Your findings seem similar to those of this paper that analyzed the dependency graph of mathlib: https://arxiv.org/abs/2604.24797 The abstract says: "taxonomies designed by humans diverge from logical structures, exhibiting a 50.9% coupling across namespaces"
Open ##2599025
-
@MartinEscardo@mathstodon.xyz Welcome to the joys of a particular flavour of meta-mathematics.
From every system (Mizar, Rocq, mathlib, Agda, Isabelle/HOL for sure), I've heard people who have dug into the de facto dependency graph marvel at how unexpected it is.
These modern tools ought to be used to teach us how mathematics is actually organized.
Open ##2599026