5 ms·

Someone in another comment also mentioned the possibility of "proof libraries" that could be used to assemble more complex proofs from simpler ones. My first th

Someone in another comment also mentioned the possibility of "proof libraries" that could be used to assemble more complex proofs from simpler ones. My first thought was, "I wonder what'll happen when someone finds a suble bug on one of the most common proof libraries?" It's bound to happen, after all. Some theorems will be proven false that were true and vice versa. A few people 90% of the way through their PhD will have years of their lives swept away.

darkmighty 11y ago
The interesting thing about this is that trivial errors like this cannot happen (unless there is a bug in coq itself). For instance, I imagined using a library might be something like using a certain Theorem 1, with proof given by Proof 1. Since T1 and P1 are formalized, they've been verified! So I can only think of some nontrivial mistakes: the Theorem 1 is correct, but it doesn't prove what you assume in your head T1 is saying, so that you may build some valid but tautological claims. I don't know if that's a huge concern, but in any case it could happen without proof verifiers anyway. Disclaimer: I'm not actually a mathematician and I haven't tried coq yet (although I most certainly will! seems very interesting).
yaantc 11y ago
Check dedukti: http://dedukti.gforge.inria.fr/ http://dedukti.gforge.inria.fr/ It's a different proof assistant that can convert Coq's (and other P.A.) proofs into its own language and check them. It's not a guarantee of course, both Coq and Dedukti could have a similar bug. But it certainly helps having independent implementations being able to check the same proofs.
- axorb 11y ago
  We're talking proofs here tho, and you aren't allowed to prove something by "throwing enough input at it", isn't it like saying that unit tests are proofs of the correctness of a program?
  - OneMoreIdol 11y ago
    This is actually a valid proof technique with finite cases. This is known as a Proof by Exhaustion.
  - darkmighty 11y ago
    Well perhaps you could actually prove the correctness of coq itself. In any case it's just a matter of reliability in the traditional sense: we're going to end with a small set of statements that will have to be verified by humans upon which we can rest everything else. Those statements will need enough people looking at them to get a level of certainty we're comfortable with. I believe the risk of a major flaw going unnoticed is astronomically low, and the good thing is this certainty propagates all the way to modern proofs if we take care to go through formal verification.
  - sukilot 11y ago
    That's no different from how regular math works. The whole point of this article is that mathematics is not formally verified today -- mathematicians just spot check and probe suspicious parts using informal analysis.
eli_gottlieb 11y ago
You can't have a bug in the proof library, or the proof-checker won't accept your proof as true! You can have a bug in the proof-checking kernel which makes it accept false theorems, but that's precisely why we keep proof-checking kernels as small and well-debugged as possible, sometimes going so far as to formally verify them too (Coq in Coq[1]). [1] http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf
sukilot 11y ago
Note that this already happens today. Mathematicians get a prestigious appointment based on a breakthrough work, which is then proven to be a mistake.

darkmighty 11y ago

The interesting thing about this is that trivial errors like this cannot happen (unless there is a bug in coq itself). For instance, I imagined using a library might be something like using a certain Theorem 1, with proof given by Proof 1. Since T1 and P1 are formalized, they've been verified! So I can only think of some nontrivial mistakes: the Theorem 1 is correct, but it doesn't prove what you assume in your head T1 is saying, so that you may build some valid but tautological claims. I don't know if that's a huge concern, but in any case it could happen without proof verifiers anyway. Disclaimer: I'm not actually a mathematician and I haven't tried coq yet (although I most certainly will! seems very interesting).

yaantc 11y ago

Check dedukti: http://dedukti.gforge.inria.fr/ http://dedukti.gforge.inria.fr/ It's a different proof assistant that can convert Coq's (and other P.A.) proofs into its own language and check them. It's not a guarantee of course, both Coq and Dedukti could have a similar bug. But it certainly helps having independent implementations being able to check the same proofs.

axorb 11y ago
We're talking proofs here tho, and you aren't allowed to prove something by "throwing enough input at it", isn't it like saying that unit tests are proofs of the correctness of a program?
- OneMoreIdol 11y ago
  This is actually a valid proof technique with finite cases. This is known as a Proof by Exhaustion.
- darkmighty 11y ago
  Well perhaps you could actually prove the correctness of coq itself. In any case it's just a matter of reliability in the traditional sense: we're going to end with a small set of statements that will have to be verified by humans upon which we can rest everything else. Those statements will need enough people looking at them to get a level of certainty we're comfortable with. I believe the risk of a major flaw going unnoticed is astronomically low, and the good thing is this certainty propagates all the way to modern proofs if we take care to go through formal verification.
- sukilot 11y ago
  That's no different from how regular math works. The whole point of this article is that mathematics is not formally verified today -- mathematicians just spot check and probe suspicious parts using informal analysis.

eli_gottlieb 11y ago

You can't have a bug in the proof library, or the proof-checker won't accept your proof as true! You can have a bug in the proof-checking kernel which makes it accept false theorems, but that's precisely why we keep proof-checking kernels as small and well-debugged as possible, sometimes going so far as to formally verify them too (Coq in Coq[1]). [1] http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf

sukilot 11y ago

Note that this already happens today. Mathematicians get a prestigious appointment based on a breakthrough work, which is then proven to be a mistake.