I'm looking for recommendations for frameworks/tools/setups that could facilitate machine checked math manipulations.

More details:

• My current use case is to show that an optimized reshuffling of a big matrix computation is equivalent to the original unoptimized expression
  • Need to be able to index submatrices of an arbitrary sized matrices
• I tried doing the manipulations with some CASes (SymPy and Mathematica), which didn't work at all
  • IIUC the main reason they didn't work is that they couldn't handle the indexing thing
• I have very little experience with proof assistants, and am not willing/able to put the effort into becoming fluent with them
• The equivalence proof doesn't need to be a readable by me if e.g. an AI can cook up a complicated equivalence proof
  • So long as I can trust that it didn't cheat e.g. by sneaking in extra assumptions