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
LW feature request/idea: something like Quick Takes, but for questions (Quick Questions?). I often want to ask a quick question or for suggestions/recommendations on something, and it feels more likely I’d get a response if it showed up in a Quick Takes like feed rather than as an ordinary post like Questions currently do.
It doesn’t feel very right to me to post such questions as Quick Takes, since they aren’t “takes”. (I also tried this once, and it got downvoted and no responses.)