Our first Drosophila for studying creative solutions is the mutilated checkerboard problem.
Two diagonally opposite corner squares are removed from a
checkerboard. Is it possible to cover the remaining squares with
dominoes? A domino is a 
rectangle, i.e. can cover
two rectilinearly adjacent squares.
The standard proof that this is impossible notes that a domino covers one black square and one white square, and therefore any covering by dominoes covers equal numbers of squares of the two colors. However, the mutilated checkerboard has 32 squares of one color and 30 squares of the other color.
We regard this proof as creative, because it involves an element not present in the formulation of the problem--namely the colors of the squares.
Here's a concise expression of the idea.
A domino covers two squares of opposite color.
For some people this will be enough. Others may require the additional sentence
The two squares that have been removed are of the same color.
One could argue that the colors are present implicitly when a
checkerboard is mentioned, and perhaps the problem would be purer if
it referred to an 
array. However, one's initial reaction
to the problem is to consider there being two colors as irrelevant,
just as it is irrelevant what the two colors are--some boards have
black and white squares, some have red and black, and some have green
and off-white (perhaps thought to be more relaxing for the players).
[McCarthy 1964] presented the problem as a tough nut for first order theorem provers, because a straightforward formalization of the problem provides no way of making the argument in the language of the formalization. Creativity was not mentioned in that 1964 memo, but I evidently mentioned it in lectures, because the problem gave rise to an informal competition aimed at finding the most non-creative solution to the problem.
The first ``non-creative'' solution was proposed by Shmuel Winograd of IBM. He claimed it was non-creative, because it didn't involve coloring.
Assume a covering. The number of dominoes projecting from the top row to the second row is odd. Likewise the number from the second to the third is odd, etc. Therefore, the total number of vertical dominoes is the sum of seven odd numbers and hence odd. Likewise the the number of horizontal dominoes is odd. Odd + odd is even so the total is even, but the total is 31. There is an apparent mathematical induction here in the ``etc.''. We will see later that the idea itself does not include the induction.
Surely Winograd's proof is creative, but we can ask whether there is one creative idea in it or several. My guess is that there was one creative idea, and the rest was straightforward for a good mathematician like Winograd.
The second was by Marvin Minsky of M.I.T.
Start with the 2-diagonal next to an excluded corner square. 2 dominoes must project from it to the adjacent 3-diagonal. Subtracting, one domino projects from the 3-diagonal to the 4-diagonal. 3 project from the 4-diagonal to the 5-diagonal, 2 project from the 5-diagonal to the 6-diagonal, 4 from the 6-diagonal to the 7-diagonal and finally 3 project from the 7 diagonal to the 8-diagonal. This covers only 3 of the 8 squares in the 8-diagonal. Coming from the opposite excluded corner also only covers 3 squares of the 8-diagonal, leaving 2 uncovered squares. Minsky's proof gets high points for non-creativity, because it is specific to the 8 by 8 board.
The third method is by Dimitri Stefanuk of Moscow, Russia. He suggested 62 proofs--or 17, taking into account symmetries.
Choose an arbitrary square and mark it 1. Mark its rectilinear neighbors 2, their unmarked neighbors 3, continuing until every unexcluded square is marked. Then proceed as in Minsky's proof, counting the number of dominoes projecting from the 1-squares to the 2-squares, etc. We get a proof if there are not enough dominoes projecting from the n-1 squares to the n-squares. Every attempt at a Stefanuk proof succeeds. Stefanuk proofs are just as uncreative a Minsky proofs.
Remark: Counting colors shows that Stefanuk proofs and Minsky proofs always work on any even board. However, this argument is at a meta-level to the Minsky and Stefanuk proofs and therefore can't claim to be non-creative.
In fact, the Winograd, Minsky and Stefanuk proofs are all creative, and we will try to identify the creativity involved and give a concise expression of the ideas.
The most recent proofs, by separate computer programs written by Mark
Stickel ([Uribe and Stickel 1994]) and Dan Pehoushek (personal
communication) apply propositional satisfaction algorithms to a
propositional expression in 256 variables. There is a variable
asserting for each square and each of the four direction whether a
domino projects from that square in that direction.
The propositional satisfaction proofs are genuinely non-creative, and but because they come from computer programs. Writing the propositional calculus formulas asserting that a domino projects in exactly one direction from each square, that there is a domino project back from a square into which a domino projects and that no domino projects off the board or into a forbidden square is taken as straightforward, i.e. not involving creativity.
[Subramanian 1993] includes an interactive proof using the Boyer-Moore prover NQTHM. Allen Newell also discussed the problem.