i know i go on about this but mathematical notation is like a programming language where there is a single global namespace for everything, no objects or encapsulation, and function / variable names are only allowed to be one character long
why are we not fixing this
mathematical proofs have 3 main uses: to give (albeit contingent) certainty, to give understanding, and to serve as a tool / component in reasoning, and imo the traditional model falls down in all three.
it makes sense why we ended up here, historically, but we've learned a lot in the last few decades about how to make formal structures useful and readable by humans and almost none of it has percolated back to mainstream mathematics