# Formal verification in complexity theory

Reading books and papers on complexity theory, I am struck by the extreme degree to which proofs are stated in an intuitive, hand-wavy way. The alternative is to give a lot of details about the coding of complicated Turing machines which simulate each other. Even proofs which basically take one line for a person to understand would take pages and pages if you actually specified the Turing machines.

Have formal verifications of complexity theory results been written? If so, to what extent does this require coding all the horrible Turing Machine details and how much does this blow up the proofs by?

-
I can't see why you would ever want to work directly with Turing machines even if you were interested in being more rigorous. Wouldn't you just work with some convenient Turing-complete programming language? –  Qiaochu Yuan Sep 27 '11 at 21:05
In complexity, Turing-completeness is not enough. If you want to prove something about the complexity of a language with respect to, say, Turing machines, then you need to take a language with equivalent time/space characteristics to Turing machines. This may cause extra logarithmic or polynomial factors to come in. This may or may not be considered unimportant. Even if you go to another Turing-complete language, there is still an unavoidable amount of coding. –  David Harris Sep 27 '11 at 21:11
The extra factors are, as you indicated, at worst polynomial, so they won't matter for complexity classes like P and NP. For smaller classes, like linear time, you probably don't want to use Turing machines anyway. Gurevich and Shelah have a theorem that says linear-times-polylog time is the same for all the usual computation models except Turing machines. –  Andreas Blass Sep 27 '11 at 21:25
This is not to dissimilar to the way people often argue about homotopies. More often than not, homotopies are described in high level language because a specific formula for the homotopy is usually tedious to write down and more often than not is unenlightening. –  Benjamin Steinberg Sep 27 '11 at 21:58

Generally complexity theorist prefer to use as little formalism as possible. $\mathsf{IP}=\mathsf{PSpace}$ is on the list here but it doesn't seem that it has been verified with a proof assistant.

I doubt that complexity theorists would be interested in writing formal proofs verifiable by proof assistants unless there is very good incentive to do it. Making proofs more formal might make it easier for proof assistants to verify them, but it makes them much less readable by humans.

But if you want more detailed analysis of the proofs, some results and theorems have been studied in bounded reverse mathematics, you can find more on this in the papers by Steve Cook and some of his students, in particular Nguyen's thesis. Also Alexander Razborov has a few papers where he studies the required theories to prove complexity results like switching lemma and Smolensky's proof of Razborov-Smolensky.

-