Post #2599025

@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"