🚀 go-pugleaf

    Mathematics would also be placed in a surprising position by P=NP.
    P=NP implies that there is an algorithm which, given a theorem
    expressed formally in ZF, say, and a number n, either gives a formal
    proof of the theorem of length at most n, or shows that there is none,
    and which would take time bounded by some polynomial in n. It wouldn't
    *necessarily* put us all out of the math research business, but....

I don't know that this is really so interesting: the kinds of things
we write down in mathematical proofs ("by symmetry, X, and by
induction on n, Z") often would have very large expansions in formal
proofs.  The kind of thing a mathematician would write down as a proof
of a theorem is less like shorthand for a formal proof than like a
computer program which generates a formal proof.  So we're not so
interested in the length of the formal proof as in the length of the
shortest such program.  But recognizing whether a program P generates
a proof of a theorem T is not in NP---it's not even undecidable
(because we can't even tell if P ever halts).  Thus, my feeling is
that even an NP-oracle wouldn't put mathemeticians out of business.