 In the current context, the central question is not whether computer-based mathematics is ‘experimental’ but whether it is—at least sometimes—non-deductive. In one sense, of course, all of the individual calculations performed by a computer are deductive, or at least they are isomorphic to the operations of a purely deductive formal system. When a computer verifies an instance of GC, this verification is completely deductive. We may then separate out two distinct questions. Firstly, are these computations playing a non-deductive role in some larger mathematical argument? And, secondly, are the beliefs we form directly from the results of computer computations deductively grounded beliefs? The first of these questions does not turn on anything specific to computers, and hence collapses back to the issue discussed in Section 3(B) above on enumerative induction. The second question will be examined below.