Wow, this seems convoluted. I used this formula:

ISBLANK( Account.Id ) == FALSE && ISBLANK(MailingPostalCode) == false && MailingPostalCode <> Account.ShippingPostalCode

And in my own tests, it works fine.Note that the instructions require "A contact with a MailingPostalCode that has an account and does not match the associated Account ShippingPostalCode should return with a validation error and not be inserted." - the above examples do not check for MailingPostalCode, as far as I can tell. Note too that the create contact form - at least in my instance - does not even acccept an address on insert, only after, on update, so I am only able to full test on update, not insert.

At any rate, I am able to add and edit contacts with correct blocking only when I have both an account and mailing address, and their postal codes don't match. But, trailhead tells me that "The validation rule failed to enforce the business logic".

So, I changed to the logic given in Paul Osnes' answer, and it works the same in real life, but now the challenge passes too.

AND( 
    NOT(ISBLANK(AccountId)), 
    NOT(ISBLANK(Account.ShippingPostalCode)), 
    MailingPostalCode<>Account.ShippingPostalCode 
  )

I suppose that means that the challenge is looking for what it thinks is the right answer, not actually testing that the logic works? Sorry to tag a question onto another - it's really more for benefit of others in my boat, though I'd be able for confirmation that this is what is going on.