The Metamath Proof Explorer (AKA the set.mm database) works on a similar principle, of all theorems forming a tree of backreferences that ultimately lead to the axioms [0].

Though it wouldn't make sense to build something like that on top of such a fast-moving, complex, and bug-prone target like Lean.

[0] https://us.metamath.org/mpeuni/mmset.html