Hacker News new | ask | show | jobs
by dagw 3682 days ago
Computer assisted proofs are historically frowned upon because you eventually end up in a black box you have to blindly trust. Can you verify that your code is correct according to the language spec? Can you verify that your compiler is bug free and follows the spec? Can you verify that your CPU is bug free and runs the output from your compiler correctly? Can you verify that your storage medium is correct and hasn't corrupted any of your intermediate results etc. etc.

Practically people will eventually say that if your test has been run N times using M different compilers and P different computers and they all give the same answer then you're probably correct, but having a proof that humans can reason through from beginning to end makes people feel more comfortable.

That being said computer assisted proofs are becoming more and more common and mathematicians are getting more and more comfortable with them as the verification tools surrounding them keep getting better. And even if computers aren't used for the final proof they are often used for intermediate tests. For example if you're making a statement about all primes it makes sense to quickly test the first few hundred million primes to make sure there aren't any obvious counter-examples.
2 comments
thfuran 3682 days ago
>it makes sense to quickly test the first few hundred million primes to make sure there aren't any obvious counter-examples

It's kind of absurd the sorts of endeavors which computers have rendered not only possible, but relatively trivial.

link
throwawaykeno 3682 days ago
FWIW the answer to all of the questions you ask in the first paragraph is "yes, but come on, that level of skepticism is a waste of time and money". It's like demanding proof that the reviewer wasn't hallucinating when reviewing the paper.

> but having a proof that humans can reason through from beginning to end makes people feel more comfortable.

Saying that humans can't reason about computer-checked proofs is like saying humans can't reason about source code; which is to say, it's obviously false in the general case.

link