I don't think this is going to be possible until computers are smart enough to understand high level maths (theorem provers have still a long way to go). A hundred different fields of research have a hundred different notations which are usually assumed to be convention and the reader is expected to know about these. The i in the summation could also refer to the imaginary unit but only if you are talking to physicists/mathematicians. Engineers use a j instead. Or what about conventions such as Einstein summation or infix operators defined by a set of axioms? How do you even recognize what a variable is or that \oplus is likely an operator or that z^*z is not a typo but a superscript indicating complex conjugation followed by an implicit multiplication symbol?
In addition, much of the math out there is described in words, rather than pure formulae. Humans are capable to reason about these things because we are trained to have an abstract understanding of what these things mean in a given context (and we can actually understand text).
A naive implementation of checking correctness of equations would likely return an incomprehensibly long list of cases where your equation might not make sense. A program that could check each and every step of your computation needs to understand your notation and definitions. While this is possible in principle – I assume you could do that for one particular problem with Mathematica – it would take you at least a few orders of magnitude more time to implement your sanity-check program for a particular problem than to check your equations by hand.
In addition, much of the math out there is described in words, rather than pure formulae. Humans are capable to reason about these things because we are trained to have an abstract understanding of what these things mean in a given context (and we can actually understand text).
A naive implementation of checking correctness of equations would likely return an incomprehensibly long list of cases where your equation might not make sense. A program that could check each and every step of your computation needs to understand your notation and definitions. While this is possible in principle – I assume you could do that for one particular problem with Mathematica – it would take you at least a few orders of magnitude more time to implement your sanity-check program for a particular problem than to check your equations by hand.