Is P=NP relevant to finding proofs of everyday mathematical propositions?

Let me address the issue at the beginning of the original question: If P=NP were proved and an algorithm with reasonable constants found, would mathematicians stop trying to prove things? The relevant NP set in this situation seems to be the $L_1$ of Ryan Williams's answer, which I regard (or decode) as the set of pairs consisting of a proposition $P$ to be proved and an upper bound $n$, written in unary notation, for the proof length. If we had a polynomial time algorithm for this NP set, then I could apply it as follows. Take $P$ to be some proposition that I'm tempted to work on, and take $n$ to be larger than any proof that I'd have time to write out in my life. If the algorithm, applied to these inputs, says "no" then I shouldn't work on this problem, because any proof would be too long for me to write out. If the algorithm says "yes" then I still shouldn't work on the problem because a P-time algorithm for Ryan's $L_2$ could find the proof for me. All of this, however, depends on an extremely optimistic understanding of "reasonable constants". The $n$ I chose is (I hope) rather big, so even a quadratic-time algorithm (with a small coefficient on the quadratic term) could take a long time (longer than my lifetime).

The bottom line is that, if P=NP were proved with plausible constants in the running time, it would not be foolish for me to keep trying to prove theorems. (Even if it were foolish, I'd keep trying anyway, partly because it's fun and partly because people might like my proof better than the lexicographically first one.)

By the way, the system in which proofs are done should, for these purposes, not be simply an axiomatic system like ZFC with its traditional axioms and underlying logic. It should be a system that allows you to formally introduce definitions. In fact, it should closely approximate what mathematicians actually write. The reason is that, although I'm looking only for proofs short enough to write in my lifetime, that doesn't mean proofs short enough to write in primitive ZFC notation in my lifetime. I believe some (if not all) of the proofs I've published would, if written in primitive ZFC notation, be too long for a lifetime.

I myself think that proving that P=NP is neither necessary nor sufficient for getting computers to solve mathematics problems.

Not sufficient: it could produce long and virtually meaningless certificates of truth rather than proper proofs that we can actually understand and be interested in.

Not necessary: as mathematicians we do not solve the fully general problem, "Is there a proof of this statement that takes fewer than n symbols?" Rather, we focus on a very small subclass that consists of interesting and meaningful problems and we search for interesting and meaningful proofs. I myself believe that this problem is solvable in polynomial time (roughly speaking because I don't believe that humans have special abilities that computers will for ever lack).

Let me try a slightly more detailed answer than the previous ones. I don't know if it clears up your concerns, because I'm not completely sure what your concerns are. For any proof system, consider the languages

$L_1 = \{ P1^n ~|~n \in {\mathbb N}$ and Proposition $P$ has a proof in the system with at most $n$ symbols$\}$.

$L_2 = \{ P1^k ~|~n \in {\mathbb N}$ and Proposition $P$ has a proof in the system and the $k$-th bit of the lexicographically first proof of $P$ is 1$\}$.

If $P=NP$, then the two above languages can be solved in polynomial time (for "everyday" proof systems). This allows you to produce a proof of any fixed proposition $P$, when it exists, in time that is polynomial in the length of the shortest proof. We do not need to know the length of the shortest proof in advance. For example, if SAT is solvable in linear time (an open problem), then the below procedure should be implementable in no more than quadratic or cubic time in the length of the shortest proof.

I will outline why this is true. Suppose for explicitness that the running time for deciding both $L_1$ and $L_2$ is at most $c \cdot n$ where $n$ is the input length. First, run the program for $L_1$ on $P1$, $(\neg P)1$, $P1^2$, $(\neg P)1^2$, $P1^4$, $(\neg P)1^4$, $P1^8$, $(\neg P)1^8$, etc., until the program outputs "yes". The running time of this procedure is about $c(d+2)2^k$ where $d$ is the length of the proposition and $2^k$ is the smallest power of two that exceeds the length of the shortest proof. This determines an upper bound on the length of the shortest proof up to a multiplicative factor of two. (By performing a "binary search" in a similar way on the interval $[2^{k-1},2^k]$ with a slightly modified language, you could uncover the minimum length of a proof if you like, call it $p$. For us it suffices to have a good upper bound on the length.)

Suppose the program output "yes" on $P$ (rather than $\neg P$). Then run the program for $L_2$ on $P1^1$, $P1^2$, $\ldots$, $P1^p$ (or up to $P1^{2^k}$). Each call returns a bit of the lexicographically first proof of $P$ which has length $p$. The total running time is about quadratic in $p$ (with some extra constants $c$ and $d$).

If you're arguing that even this sort of running time must still be impractical for "everyday mathematical propositions", I would have to disagree. If the constant $c$ in the algorithms were provably gigantic (or more generally, the degrees of the polynomials in the running time) then this would be true, but we have very little knowledge of bounds on $c$ at this time.