I am not aware of any good one, but I realized you could probably mechanically extract such a map from Lean's mathlib[0][1]. Since Lean builds everything from

I am not aware of any good one, but I realized you could probably mechanically extract such a map from Lean's mathlib[0][1]. Since Lean builds everything from scratch, this should be doable, albeit Lean builds everything on top of type theory which is not the only choice possible. Different foundations will result in a different graph. Also the best way to learn math is probably not by following this sort of graph, it would be far too abstract and disconnected from both the real world and usual practical applications. [0] https://leanprover-community.github.io/mathlib4_docs/ https://leanprover-community.github.io/mathlib4_docs/ [1] https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4