Strassen's Algorithm proof
The main idea of the algorithm is to find a way to multiply two $n\times n$ matrices with less than $n^3$ "essential" multiplications (multiplications of two elements of the matrices). This forms part of a larger theory, algebraic complexity theory. Here are a few highlights:


Every algorithm for multiplying two matrices can be formulated (at a small loss) as a bilinear algorithm: you form some linear combinations $\alpha_1,\ldots,\alpha_k$ of entries of the first matrix, some linear combinations $\beta_1,\ldots,\beta_k$ of entries of the second matrix, compute $\gamma_i = \alpha_i \beta_i$, and then every entry of the product matrix is a linear combination of the $\gamma_i$.
This can be formulated as computing the tensor rank of the matrix multiplication tensor $\langle n,n,n \rangle = \sum_{i=1}^n\sum_{j=1}^n\sum_{k=1}^n x_{ij} y_{jk} z_{ik}$. The tensor rank is similar to the more familiar matrix rank, and corresponds to the number of "essential" multiplications ($k$ in the preceding example).
Any non-trivial bound on $\langle n,n,n \rangle$ for any $n$ translates to a non-trivial matrix multiplication algorithm for all $n$, via the same recursive approach as Strassen's algorithm (this approach is also known as tensorization). There are several extensions, culminating in Schönhage's asymptotic sum inequality.
The asymptotic sum inequality can handle identities involving disjoint sums of matrix tensors (in plain English, ways of multiplying several matrices at once using fewer "essential" multiplications than the trivial algorithm uses), and can even handle "approximate" identities (border rank). Strassen came up with another method (the laser method) that can handle non-disjoint sums, and this led to the Coppersmith-Winograd algorithm and its descendants, which is where things stand today.