Human mathematical creativity is not reducible to computation. An illustration of this is that human beings would have an easier time figuring out Bourbaki's Set theory. As A. Mathias showed, Bourbaki's definition of "1" requires billions of characters. The definition of "2" is probably inaccessible to modern computers. The Bourbaki definition is certainly inefficient from the computational standpoint, but the point is that a (human) reader can follow the reasoning without being able to process a billion chips.