In combinatorics, one can sometimes get an algorithmic proof, which loosely has the following form:
-The proof moves through stages
-An invariant is shown to hold by induction from previous stages
-The algorithm is shown to terminate
-The invariant holding at termination implies the desired claim.
Perhaps the best example I know of is an algorithmic proof of Konig's theorem, which in a sense is just a max-flow/min-cut algorithm. In some sense, most induction proofs fit this mold.
The above example runs in polynomial time. Are there good examples of algorithmic/induction proofs that take super-polynomial time to prove things that don't obviously need such induction?
That is, I don't want Ackermann-like recurrences, or anything that is "brute-force". Further, I'm not looking for super-polynomial time algorithms that solve instances of problems, but rather am looking for super-polynomial time algorithms that prove a theorem of some sort (eg. like a combinatorial max-min theorem in the above example).
Best Answer
The standard proofs of Sperner's Lemma are the first thing that comes to my mind in this context. They don't have exactly the form you mentioned; in particular they're not really inductive. Nonetheless, the proofs use a path-following algorithm which may take exponential time but is guaranteed to terminate for combinatorial reasons.
In fact the complexity class PPAD is defined as those problems for which such a path-following argument proves existence, and "SPERNER" is a PPAD-complete problem. It is an open problem whether such problems can be solved in polynomial time (I think most people guess not). Furthermore just by definition all the other PPAD-complete problems (or PPAD problems in general) have the form you want, i.e. and algorithmic existence proof.
There are a number of other such complexity classes defined in terms of types of non-polynomial-time existence proofs. Examples are PPA, PLS, etc. See Papadimitriou's paper "On the complexity of the parity argument and other inefficient proofs of existence" for more examples.