# Theorem Prover for complexity theoretic reductions

Can complexity theoretic reductions that lead to proofs of say NP completeness be formalized using an existing theorem prover such as Coq?

If so, can you provide an outline of how to formalize a simple reduction argument? I’d also appreciate pointers to the literature.

• The belief is that all mathematical arguments can be formalized in Coq. NP-hardness reductions are mathematical arguments. The only conclusion is... – Yuval Filmus Nov 10 '17 at 6:24

Theorem reduction:

What gets tricky is proving that your reductions are polynomial-time. There are ways to do this, such as with a time-tracking monad. This example verifies the time complexity of a sorting algorithm, and gives some hints as to how to model this. Basically, for whatever operation you're counting as $O(1)$, you require that it be performed in the monad, as well as calls to your oracle. Then you write a proof of some polynomial bound on the number of operations performed in the monad (which can keep track of them by encapsulating state).