Neither did Gödel's automatic theorem prover require "human ingenuity or creativity required to carry out the steps" to enumerate all the theorems from the axioms, which are also enumerable. Gödel really described "the heart of what it means to be computable."