Here is a question I thought of this morning, and have given no serious thought to — hence, perfect for a blog post.
In any commutative ring, if and are matrices, and , then .
For any fixed , there should be a proof of this by direct algebraic manipulation: Start with the equations saying that , and add, multiply, expand and recombine them to produce the equations saying that . Our starting point is equations of size , as is our destination. But every route I see involves writing down the adjoint of or , which is an expression of length .
Can we show that a direct proof of this result must involve either an expression of exponential length, or an exponentially long proof?