IMO mathematics benefits from being highly generic compared to normal code, so much so that the implementation itself doesn't really matter (and it's entirely normal in mathematics to skip details, unlike in software). So then to me it makes sense to have a clean separation between basically header files and implementation files like in C and C++. Then something like mathlib should be a pristine collection of what belongs in headers: data structure definitions, instances, theorem statements, macros/tactics for common techniques, etc. So basically it is a curated set of "axioms" that can be used for other math and remain understandable, indexable, etc. Maybe a companion mathlib-full that can actually compile the entire theory.

I suppose this could be done with just tooling to generate a skeleton/index of a giant repository of all mathematics if you decided that you're going to index all definitions and theorems but not lemmas or examples or something like that.