My question concerns what is meant by "nonconstructive", and whether it has ever been defined in terms of computational complexity.
The wikipedia article on constructive proof begins, "a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object." On the other hand, the wiki article on the probabilistic method states, "the probabilistic method is a nonconstructive method [...] for proving the existence of a prescribed kind of mathematical object." I believe these two statements are at odds with one another.
Consider Erdős's celebrated proof of the lower bound of the Ramsey number. This proof shows that as long as $\binom{n}{r} < 2^{\binom{r}{2} - 1}$, there is some coloring of the edges of $K_n$ with $2$ colors that has no monochromatic sub-$K_r$. The proof offers no idea what such a coloring looks like; however, it does lead to a "method for creating" the object in question: try all possible colorings. The proof guarantees that this naive algorithm terminates. Of course, this algorithm quickly becomes computationally infeasible. But in principle, via exhaustive search, any proof of the existence of an object in some finite collection admits of a "method for creating" the object.
Imagine now that we had a different proof of the lower bound of the Ramsey number. This new proof constructs two possible edge-$2$-colorings of $K_n$ and shows that at least one must result in no monochromatic sub-$K_r$, although it remains silent about which of the two colorings works. I think this would also qualify as a "non-constructive" proof (based on analogy to the wiki example with $\sqrt{2}^{\sqrt{2}}$), and yet it would lead to a wonderfully efficient method for finding such colorings. For any $r$, this hypothetical proof says we have to check only two candidates to get the object we're looking for. I think this even gives us a polynomial time algorithm for finding such a coloring (but this depends on how quickly we can verify a coloring.) At any rate, I hope the distinction I am trying to draw is clear.
Does it makes sense to say that a constructive proof is a proof that leads to an efficient algorithm for creating an object with a desired set of properties? Has there been any work related to such a definition? The above is most relevant to statements in discrete math.