I think it will when we finally have a language that is useful for all of: jotting down expressions, manipulating them by hand, and being consistent enough that

I think it will when we finally have a language that is useful for all of: jotting down expressions, manipulating them by hand, and being consistent enough that automated theorem provers/proof helpers can use as their internal representation. 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.