Examples of Super-polynomial time algorithmic/induction proofs? 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).
 A: 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.
A: I agree with Noah that Papadimitrou's classification of several cannonical types of algoritmic proofs is very relevant to the question and to the understanding the computational complexity of mathematical existence proofs. 
Another interesting class is described by finding the sink in acyclic unique sink orientations (AUSO) of the didcrete n dimensional cube. Those are orientations of the discrete cube so that every face has a unique sink. There is an algorithm to find the sink in $exp (\sqrt n )$ steps. 
Another algorithmic proof whose complexity is unknown is Barany's proof of colored caratheodory theorem.  
A: The Hydra game:


*

*http://math.andrej.com/2008/02/02/the-hydra-game/
I'm not sure if that counts as an "Ackermann-like recurrence" but the algorithm is super-duper-exponential and then some.  It's not even possible to write down a formula for the running time, but it definitely terminates.
A: Another example is the matroid intersection theorem, which is a rich source of min/max theorems in combinatorial optimzation.  For example, it includes your example (Kőnig's theorem) as a special case.  
There is an algorithmic proof of the matroid intersection theorem which runs in time polynomial in $|E(M_1)|$, $|E(M_2)|$, and the running-times of the independence oracles for $M_1$ and $M_2$.  Therefore, we get proofs which run in super-polynomial time whenever we have a matroid which cannot be described by an efficient independence oracle.  
