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

-

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.

-