Along the same lines, does there exist an "algebra checker" that could, say, take in two successive lines of latex, with perhaps a hint of how to get from one to the other, and confirm that there are no algebra errors?
SymPy does not take Latex as input, but it has symbolic equivalence checkers. Methods are highly heuristic, and some languages (all expressions with,say, \pi, and exp function, or something similar) are in general undecidable.
import sympy
from sympy.abc import x, y, alpha, s
quad = s ** 2 - alpha * s - 2
# Let s1 and s2 be the two solutions to the quadratic equation 'quad == 0'
s1, s2 = sympy.solve(quad, s)
u = (x - s2) / (x - s1) * (y - s1) / (y - s2)
f1 = (s2 - s1 * u) / (1 - u)
f2 = (x * y - alpha * x - 2) / (y - x)
# Claim: f1 is equal to f2
print(sympy.simplify(sympy.Eq(f1, f2)))
# Prints "True"