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.
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" >>> 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