  The Tensor Isomorphism problem (TI) has recently emerged as having
connections to multiple areas of research within complexity and beyond, but the
current best upper bound is essentially the brute force algorithm. Being an
algebraic problem, TI (or rather, proving that two tensors are non-isomorphic)
lends itself very naturally to algebraic and semi-algebraic proof systems, such
as the Polynomial Calculus (PC) and Sum of Squares (SoS). For its combinatorial
cousin Graph Isomorphism, essentially optimal lower bounds are known for
approaches based on PC and SoS (Berkholz & Grohe, SODA '17). Our main results
are an $\Omega(n)$ lower bound on PC degree or SoS degree for Tensor
Isomorphism, and a nontrivial upper bound for testing isomorphism of tensors of
bounded rank.
  We also show that PC cannot perform basic linear algebra in sub-linear
degree, such as comparing the rank of two matrices, or deriving $BA=I$ from
$AB=I$. As linear algebra is a key tool for understanding tensors, we introduce
a strictly stronger proof system, PC+Inv, which allows as derivation rules all
substitution instances of the implication $AB=I \rightarrow BA=I$. We
conjecture that even PC+Inv cannot solve TI in polynomial time either, but
leave open getting lower bounds on PC+Inv for any system of equations, let
alone those for TI. We also highlight many other open questions about proof
complexity approaches to TI.
