We define
Making this definition is a creative step, but it doesn't give the solution by itself.
This is the key creative step.
and finally
Q.E.D.
This last step is presumably routine.
[McCarthy 1996] argued that the above proof, or some equally concise expression of its ideas, should be accepted by any mathematical proof checker that mathematicians would actually use. Unfortunately, no present proof checker comes close.
The following two definitions are used in the proofs by Winograd, Minsky and Stefanuk.
and
I suppose they count as creative, but maybe as one creation rather than two.
In a future article, we hope to put the Winograd and Stefanuk proofs in a logical form that isolates the creative part from the routine part.
