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.
Best Answer
As others have noted there are several different meanings for constructive.
I. Constructive proof in the sense of constructive mathematics
This meaning views an object as existing if we have a description of how to construct the objects (though we don't really need to carry it out), and there are several distinct constructive views. Saying a proof is constructive or not can be ambiguous without specifying which school of constructive mathematics we are talking about.
By the way, it can be the case that we can convert a non-constructive proof to a constructive one (Georg Kreisel's unwinding program or Ulrich Kohlenbach's proof mining program). That does not make the original proof constructive!
Note that algorithmic computability is just one of several constructive perspectives. For example, in intuitionism there are objects which are not algorithmically computable. A way of understanding this is to remember that Churth-Turing thesis is not an axiom that is accepted by all constructivist, there can be constructions which are not algorithmic in the instuitionistic view.
II. Constructive in the sense of complexity theory
This is a more recent meaning. We mean a proof of existence of an object is constructive if it gives directly a method of efficiently computing/constructing the object. This is the more common meaning of the word in combinatorics these days, e.g. in Robin A. Moser's "A constructive proof of the Lovasz Local Lemma" paper from 2008.
Constructive is used in the sense of efficient algorithms in complexity theory, for example, constructive in Alexander Razborov and Steven Rudich's "Natural Proofs" paper means that the property used in the lower-bound proof is efficiently computable.
Note that the proof itself can be non-constructive in the sense of meaning I while remaining constructive in this sense. You can give an efficient algorithm to compute some object and the correctness and efficiency proofs can be non-constructive. We don't have many interesting examples, but a good example would be the Robertson-Seymour theorem. See also Are there non-constructive algorithm existence proofs?
III. Proof complexity perspective
This is kind of the intersection of the previous two, though I don't recall anyone refer to it as "constructive proof" (probably because they are aware of both previous meanings and don't want to confuse people further :).
Here not only the object should be computable efficiently but the correctness and efficiency proofs must use only efficient concepts. The Robertson-Seymour theorem is an example of an efficient algorithm where we don't have a proof using only efficient concepts. I can give more artificial examples to distinguish between this and the meaning in the previous section but I don't recall any other natural ones.