To elaborate: Symbolic equivalence checking for two expressions f1 and f2 can be done by seeing if sympy.simplify(sympy.Eq(f1, f2)) is sympy.true.
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"Is there something for implication or equivalence of equations? I was trying the example from Smaug123's sibling comment (https://news.ycombinator.com/item?id=15728598), but
>>> import sympy as sp
>>> x = sp.Symbol('x')
>>> sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1)))
Eq(x, -1) | Ne(x**2 + 2*x + 1, 0)
>>> sp.solve(sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1))))
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1065, in solve
solution = _solve(f[0], *symbols, **flags)
File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1401, in _solve
f_num, sol = solve_linear(f, symbols=symbols)
File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solvers.py", line 1971, in solve_linear
eq = lhs - rhs
TypeError: unsupported operand type(s) for -: 'Or' and 'int'
>>> sp.solveset(sp.simplify(sp.Implies(sp.Eq(x**2 + 2*x + 1, 0), sp.Eq(x, -1))))
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/home/user/.local/lib/python3.5/site-packages/sympy/solvers/solveset.py", line 880, in solveset
raise ValueError("%s is not a valid SymPy expression" % (f))
ValueError: Eq(x, -1) | Ne(x**2 + 2*x + 1, 0) is not a valid SymPy expression
Methods are highly heuristic, and some languages (all expressions with,say, \pi, and exp function, or something similar) are in general undecidable.