Formal verification in complexity theory - MathOverflow

Formal verification in complexity theory

2011-09-27T21:02:44Z

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?

Answer by Timothy Chow for Formal verification in complexity theory

2011-09-27T21:31:16Z

The same comment and question could be applied to just about any area of mathematics. To my knowledge, nobody has really worked on formalizing computational complexity theory. Formalization is still hard work; an experienced person will take about a week to formalize about a page of an undergraduate textbook. Therefore, people have mostly focused on "flashy" theorems, for which you can get some kind of recognition for the work that you put into writing up the formal proof. Formalizing routine undergraduate material is a time-consuming task for which almost nobody will thank you (or pay you).

If you do write a formal proof, then of course you need to give all the details. However, sometimes you can do better than the most naive approach of literally mimicking the original human proof. For example, when Gonthier formalized the proof of the four-color theorem, he figured out ways to slicken the proof and make it easier to formalize, as he explained in his Notices article. Most likely, if a serious effort were made to formalize large chunks of computational complexity theory, shortcuts would be devised so that (to address your specific question) Cook- or Karp-reductions from one problem to another could be coded up in a more human-friendly form, with the computer automating certain parts of the process. This is not a trivial matter, though, which is why writing formal proofs is still too tedious for most mathematicians to want to contemplate.

Answer by Kaveh for Formal verification in complexity theory

2011-09-27T21:33:59Z

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.