A human proving a theorem might take it as read that 2 is a prime, or if x > y and y > z then x > z, or there are no integers between 0 and 1.

These axioms or assumptions have to be fed into an automated theorem prover. Some are deducible, others have to be either baked into the code itself or definable to the theorem prover.