Would it be possible to concoct a "harmful" axiom? Suppose I run an automated theorem prover. It begins with the axioms of ZFC, and using a random number generator, it proves more theorems, and it runs for two days. At the end of the second day, it halts.
The program then considers all the theorems it proved on the second day (but not the first), and outputs the shortest of these.
Finally, I write a paper proposing the negation of the proved statement as a new axiom of ZFC, based on some "deep intuition" I've had.
People spend lots of time working out the "profound consequences" of this new axiom. I spend lots of time laughing, and it ends up taking 100 years for people to work out that the axiom is inconsistent with ZFC.
Could this ever happen? Do the principles of computational complexity allow it to happen? And if so, what can be done about it? I don't want mathematics infected with harmful axioms.
Edit: The point is, it may be reasonably easy to use a computer to come up with a harmful axiom, but very difficult to use a computer to refute such an axiom.

Perhaps a longish comment, but we do not know if ZFC is itself consistent to begin with.  Most set-theorists (if not mathematicians in general) have a strong belief that ZFC is consistent — in part due to the fact that many brilliant mathematicians have not found a contradiction yet — but a belief is all it is.
Could an automated theorem prover come up with a theorem whose negation could not easily be refuted by humans?  Most likely, since automated theorem provers can make connections that are not immediately obvious to humans (consider the Robbins Problem which stood open for more than 60 years until William McCune used an automated theorem prover to solve it).  Might it take decades of research to discover the inconsistency?  Perhaps.  Unless, of course, if someone decided to input this all into an automated theorem prover.
