Answer from Cook: www.cs.toronto.edu/~sacook/homepage/JACMpvsnp.ps

Highlights - Computers could find formal proofs for any theorem with a reasonable length - All you need then is a good recognition algorithm for formal proofs - Then you can just work on recognizers for good novels / music / etc and have it churn out classics

The other example (I forget the source) is that if you have a P time formula for safety checking the designs of nuclear power plant, if P = NP you can efficiently generate a list of the designs of all possible safe nuclear power plants.

So you can go from P-time checkable constraints to P-time enumeration of things which fill the constraints.