3
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – Qiaochu Yuan
    Commented Sep 27, 2011 at 21:05
  • 1
    $\begingroup$ 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. $\endgroup$
    – David Harris
    Commented Sep 27, 2011 at 21:11
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andreas Blass
    Commented Sep 27, 2011 at 21:25
  • 1
    $\begingroup$ 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. $\endgroup$
    – Benjamin Steinberg
    Commented Sep 27, 2011 at 21:58

2 Answers 2

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ One other large class of theorems that have been formalised are those concerning hardware and software implementations. These include statements about data-structures, algorithms, processor architectures and the like. People do get paid for such formalisations, because finding a bug in a processor has great financial value. However, a professional mathematician (or computer scientist) would probably not call these statements theorems. $\endgroup$
    – Vijay D
    Commented Sep 27, 2011 at 23:34
3
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .