14
$\begingroup$

Considering the topics covered at a conference like STOC, are any algorithm or complexity researchers actively using COQ or Isabelle? If so, how are they using it in their research? I assume most people wouldn't use such tools because the proofs would be too low level. Is anybody using these proof assistants in a way that is critical to their research, as opposed to a nice supplement?

I am interested because I might start learning one of those tools and it would be fun to learn about them in the context of proofs of reductions, correctness, or run time.

$\endgroup$
  • 1
    $\begingroup$ Do you want to exclude "Theory B" and in particular theory of programming languages? My understanding is that proof assistants get used much more frequently in PL... $\endgroup$ – Joshua Grochow May 24 '17 at 18:20
  • 1
    $\begingroup$ I looked up the term, I guess I am focused on applications within "Theory A" $\endgroup$ – nish2575 May 24 '17 at 18:28
  • 1
    $\begingroup$ As far as I'm aware, most of Theory A is in the same category as most of the rest of mathematics: few of the foundations have been added so far to these systems, so most interesting theorems would take significant effort to first develop the infrastructure to implement the necessary definitions. There are a few interesting bits of automata theory that have been formalised, so that may be a place to look. $\endgroup$ – András Salamon May 24 '17 at 22:56
  • 1
    $\begingroup$ Results in complexity theory tend to be provable in much weaker systems, you normally don't even need PA. Coq and Isabeller are not very well-suited for complexity theory I would say. There are almost formal proof sketches like those in Cook and Nguyen's book but the main interest is to prove them in proof system related to complexity classes. Why would one like to prove them in say Switching Lemma in Coq when it can be proven in much weaker systems? $\endgroup$ – Kaveh May 25 '17 at 1:38
  • 2
    $\begingroup$ @Kaveh The weakness / strength of various proof systems is not an issue there: we'd like formally to verify proofs in complexity theory for the same reason we'd like to verify programs: to have higher degrees of reliability. In addition, it's also an interesting challenge to extend prover theory so that they can handle complexity theory proofs more conveniently. $\endgroup$ – Martin Berger May 27 '17 at 21:54
15
$\begingroup$

A general rule of thumb is that the more abstract/exotic the mathematics you want to mechanise, the easier it gets. Conversely, the more concrete/familiar the mathematics is, the harder it will be. So (for instance) rare animals like predicative point-free topology are vastly easier to mechanize than ordinary metric topology.

This might initially seem a bit surprising, but this is basically because concrete objects like real numbers participate in a wild variety of algebraic structures, and proofs involving them can make use of any property from any view of them. So to be able to the ordinary reasoning that mathematicians are accustomed to, you have to mechanize all these things. In contrast, highly abstract constructions have a (deliberately) small and restricted set of properties, so you have to mechanize much less before you can get to the good bits.

Proofs in complexity-theory and algorithms/data-structures tend (as a rule) to use sophisticated properties of simple gadgets like numbers, trees, or lists. Eg, combinatorial, probabilistic and number-theoretic arguments routinely show up all at the same time in theorems in complexity theory. Getting proof assistant library support to the point where this is nice to do is quite a lot of work!

One context where people are willing to put in the work is in cryptographic algorithms. There are very subtle algorithmic constraints in place for complex mathematical reasons, and because crypto code runs in an adversarial environment, even the slightest error can be disastrous. So for example, the Certicrypt project has built a lot of verification infrastructure for the purpose of building machine-checked proofs of the correctness of cryptographic algorithms.

$\endgroup$
6
$\begingroup$

One very prominent example is of course Gonthiers Coq formalization of the 4 color theorem in Coq which uses a lot of combinatorics.

My colleague Uli Schöpp used the ssreflect library developed by Gonthier for this purpose in order to verify (and slightly extend) also in Coq a result by Cook and Rackoff on graph automata. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). A formalised lower bound on undirected graph reachability. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 621-635). Springer Berlin/Heidelberg.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.