Isn't it an optimization to code in the type, and let the .AI work out the details necessary to implement the token ? We don't think theorem provers need to be overloaded with all known maths.

Do you mean a paperclip maximizer mistakenly believing that the English word moral means ‘optimizing paperclips’ rather than ‘optimizing life, consciousness, etc.’, or a paperclip maximizer who knows that that the English word moral means ‘optimizing life, consciousness, etc.’ but mistakenly believes that optimizing paperclips would optimize life, consciousness, etc.?

And neither is like a paperclip maximizer who knows that that the English word moral means ‘optimizing paperclips’ rather than ‘optimizing life, consciousness, etc.’, and knows that optimizing paperclips doesn't optimize life, consciousness, etc., but doesn't give a damn about optimizing life, consciousness, etc.

A paperclip maximizer optimizes as effectively as anyone else - it squuzes the future into an equally small (though different) region. A creationist would be less effective as they would make false predictions about objective facts like antibiotic resistance.

It isn't. It is, however, entirely different from a paperclip maximiser—not at all mistakenly—not caring about morality. There's no general reason to assume that a difference in goals implies a factual disagreement.