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

<p>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. <a href="https://scholar.google.at/scholar?oi=bibs&amp;cluster=4944920843669159892&amp;btnI=1&amp;hl=de" rel="noreferrer">https://scholar.google.at/scholar?oi=bibs&amp;cluster=4944920843669159892&amp;btnI=1&amp;hl=de</a> (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.)</p>

CC BY-SA 3.0
2017-11-22T15:27:55.333Z
2017-11-22T15:38:55.433Z
2017-11-22T15:38:55.433Z
Martin Hofmann
<p>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. </p>

<p>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. </p>

<p>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!</p>

<p>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 <a href="http://certicrypt.gforge.inria.fr/" rel="noreferrer"><em>Certicrypt project</em></a>  has built a lot of verification infrastructure for the purpose of building machine-checked proofs of the correctness of cryptographic algorithms.</p>

CC BY-SA 3.0
2017-05-31T15:54:33.223Z
2017-05-31T15:54:33.223Z
Neel Krishnaswami
<p>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?</p>

<p>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.</p>

CC BY-SA 3.0
2017-05-24T18:20:07.727Z
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...
Joshua Grochow
CC BY-SA 3.0
2017-05-24T18:28:19.560Z
I looked up the term, I guess I am focused on applications within "Theory A"
nish2575
CC BY-SA 3.0
2017-05-24T22:56:40.783Z
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.
András Salamon
CC BY-SA 3.0
2017-05-25T01:38:45.813Z
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?
Kaveh
CC BY-SA 3.0
2017-05-25T01:42:34.500Z
There are people generating formal proofs (through search using SAT and SMTs, not formalization existing proofs) in CS like proof of the correctness of a particular peace of hardware.
Kaveh
CC BY-SA 3.0
2017-05-27T21:52:15.467Z
Most proofs in modern proof assistants like Coq and Isabelle/HOL are highly dependent on proof automation, without which formal proofs are just too tedious. Contemporary proof automation works especially well for inductive proofs (in a general sense). However the key object of complexity theory,  *Turing machines*, is not naturally amenable to inductive methods. Consequently, proofs in complexity are unusually tedious in interactive provers, and are not being done. It would be great to improve the state of the art!
Martin Berger
CC BY-SA 3.0
2017-05-27T21:54:40.250Z
@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.
Martin Berger
CC BY-SA 3.0
2017-05-30T20:50:24.900Z
@MartinBerger: Let me put a positive spin of Kaveh's comment (if there wasn't one already): since in complexity we are often interested in how weak a proof system something can be proved in, it would be great if there were some way in Coq/Isabelle/etc. to say "Try to prove this in such-and-such weak proof system"; then we get both the benefit of formal proofs increasing reliability, and a tool for further exploring the strength of "weak" proof systems.
Joshua Grochow
CC BY-SA 3.0
2017-05-30T22:13:40.563Z
@JoshuaGrochow There is no problem in principle to prove statements like that in proof assistants. You can do a "deep embedding" of any logic in such systems and then derive the relevant theorems.  The only problem left is that this is *extremely* cumbersome if you don't have the right proof automation and infrastructure of related lemmas. There is probably several person decades work left to do before complexity theory can be carried out conveniently in provers.
Martin Berger
<cc.complexity-theory><approximation-algorithms><soft-question><proof-assistants>
Proof assistant usage in complexity theory research?
nish2575
# Proof assistant usage in complexity theory research?

(Asked by: username_0 on 2017-05-24)

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.

**Tags:** cc.complexity-theory, approximation-algorithms, soft-question, proof-assistants
> **Comments:**
> **username_1**: 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...  
> **username_0**: I looked up the term, I guess I am focused on applications within "Theory A"  
> **username_2**: 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.  
> **username_3**: 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?  
> **username_3**: There are people generating formal proofs (through search using SAT and SMTs, not formalization existing proofs) in CS like proof of the correctness of a particular peace of hardware.  
> **username_4**: Most proofs in modern proof assistants like Coq and Isabelle/HOL are highly dependent on proof automation, without which formal proofs are just too tedious. Contemporary proof automation works especially well for inductive proofs (in a general sense). However the key object of complexity theory,  *Turing machines*, is not naturally amenable to inductive methods. Consequently, proofs in complexity are unusually tedious in interactive provers, and are not being done. It would be great to improve the state of the art!  
> **username_4**: @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.  
> **username_1**: @MartinBerger: Let me put a positive spin of Kaveh's comment (if there wasn't one already): since in complexity we are often interested in how weak a proof system something can be proved in, it would be great if there were some way in Coq/Isabelle/etc. to say "Try to prove this in such-and-such weak proof system"; then we get both the benefit of formal proofs increasing reliability, and a tool for further exploring the strength of "weak" proof systems.  
> **username_4**: @JoshuaGrochow There is no problem in principle to prove statements like that in proof assistants. You can do a "deep embedding" of any logic in such systems and then derive the relevant theorems.  The only problem left is that this is *extremely* cumbersome if you don't have the right proof automation and infrastructure of related lemmas. There is probably several person decades work left to do before complexity theory can be carried out conveniently in provers.  

---

## 2 answers

### Answer by username_6 on 2017-05-31. Score: 15 | Accepted answer

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*](http://certicrypt.gforge.inria.fr/) has built a lot of verification infrastructure for the purpose of building machine-checked proofs of the correctness of cryptographic algorithms.


---

### Answer by username_5 on 2017-11-22. Score: 6

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.)


---

