To head off any confusion: I'm talking about the extremal-combinatorics Sperner's theorem, bounding the sizes of antichains in a Boolean lattice.
So the "canonical proof" of this theorem seems to be essentially Lubell's -- it's formulated in several different ways, but my favorite is this. Let $A$ be an antichain in $2^{[n]}$. Pick an arbitrary saturated chain and consider a random automorphism $\phi$ of the poset. Since $A$ is an antichain, so is the image $\phi(A)$, and the expected number of elements of $\phi(A)$ that lie in the distinguished chain is at most 1. Now if $S \subset [n]$ has k elements, then $\phi$ maps $S$ into our distinguished chain with probability $1/\binom{n}{k}$; linearity of expectation gives us the LYM inequality and Sperner's theorem follows.
This is a lovely proof, but reading over the DHJ polymath threads I heard about another approach -- apparently the approach Sperner himself used -- which one commenter described by the wonderful phrase "pushing shadows around." Evocative as this phrase is, I'm not actually sure what it means: presumably the idea is to replace an antichain by another antichain, at least as large and whose elements are "closer to the center?" This idea seems like it should work, but I can't quite get it to go through, which makes me think I'm missing something. Does anyone know the details of this proof?

