Will Computers Redefine the Roots of Math?

Re:Will Computers Redefine the Roots of Math? by tjradcliffe on Tuesday May 19, 2015 @10:22PM (#9574339)

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.

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by darkmighty on Tuesday May 19, 2015 @10:53PM (#9574409)

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

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by yaantc on Wednesday May 20, 2015 @05:19AM (#9575240)

Check dedukti: 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.

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by axorb on Wednesday May 20, 2015 @08:03AM (#9575717)

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?

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by darkmighty on Wednesday May 20, 2015 @12:07PM (#9577242)

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.

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by sukilot on Thursday May 21, 2015 @09:57AM (#9582749)

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.

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by OneMoreIdol on Wednesday May 20, 2015 @10:09AM (#9576381)

This is actually a valid proof technique with finite cases. This is known as a Proof by Exhaustion.

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by eli_gottlieb on Wednesday May 20, 2015 @10:49AM (#9576666)

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

[ Parent | on HN ]

Re:Will Computers Redefine the Roots of Math? by sukilot on Thursday May 21, 2015 @09:54AM (#9582737)

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

[ Parent | on HN ]