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).