But anytime it's brought up, mathematicians get upset. The issue will never be addressed, but it's a disaster.
The issue right now is that the impressionistic maths notation works well for humans and there is no computer language that:
1). has good notation
2). is useful to mathematicians out of the box
Mathematica, sage, axiom, etc all have internal representations that are essentially the system I'm talking about but the user facing language is a mess in all cases. It's not a simple problem and I don't even know what the solution looks like.
It will have a lispy notation (tree serialization), and use rewrite rules (generalized macros) and types (some type of type inference with explicit typing annotations), but other than that I feel like someone trying to invent Algol in 1947.