The Leibniz Prize
The Leibniz Prize was to be awarded "for the proof of a 'substantial' theorem in which the computer played a major role." The prize criteria was described as follows:
"The quality of the results should not only make the paper a natural candidate for publication in one of the better mathematical journals, but a candidate for one of the established AMS prizes (e.g., Cole, Veblen) or even a Fields Medal. The proofs should not be less sophisticated than those of classical theorems when they first made their appearance--such as, for instance, the Fundamental Theorem of Algebra or one of the fixed point theorems (Brouwer, Leray-Schauder). Though obviously difficult to define precisely, the role of the computer program in the argument should not be mere auxiliary. Novel techniques, meaningful and original definitions, suggestions of interesting intermediate results, perspectives of wider application--any one of these contributions, and others that cannot be foreseen today, would meet the criteria."
The Milestone Prize
The Milestone Prize was awarded periodically "for foundational work in ATP."
The Current Prize
The Current Prize was awarded periodically "for ongoing research in ATP that shows promise."