6 ms·

I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run i

by F-0X 8y ago

I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect computation and software is certainly not a source of perfect logic.

moomin 8y ago
They’re not, but they’re spectacularly good at spotting dumb errors that humans are spectacularly bad at spotting. Me, I still haven’t got my head around how to prove something on a computer, but the principle is sound. Theoretically one could build the proof as some form of literate program.
- chess93 8y ago
  A computer just does symbolic manipulation according to a list of rules (axioms) and the human/programmer specifies which sequence of symbolic manipulations to apply and then the computer simply states whether or not the specified manipulations transform the theorem in to the truth symbol. http://us.metamath.org/mpegif/mmcomplex.html http://us.metamath.org/mpegif/mmcomplex.html (Warning: I've never actually done much of this before so some details might be wrong.)
  - dwheeler 8y ago
    I have done some, thanks for pointing to that page! Here's a prettier version for most people (the "mpegif" version uses GIFs for math symbols, which works everywhere but doesn't look at nice): http://us.metamath.org/mpeuni/mmcomplex.html http://us.metamath.org/mpeuni/mmcomplex.html
adamnemecek 8y ago
You mean unlike human?
dwheeler 8y ago
> I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect computation and software is certainly not a source of perfect logic. The issue is not that computers are always perfect. The issue is that humans are far, far worse than computers at detecting errors in proofs. So-called proofs are later found to be wrong, even after lots of human peer review, and there are often doubts about published papers. If pure math is about proof (and it is), then checking proofs with only humans is unacceptable in the long term. Humans simply aren't good enough at it, and why should we make humans do a job (verifying proofs) when computers are obviously better at it? In addition, there are many mechanisms for countering computer errors that make their likelihood essentially zero. Hardware bugs happen, but executing software on multiple different computers using diverse CPUs basically makes that disappear. Software can have errors, but there are ways to counter that too. The Metamath community verifies set.mm (its main database at http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ) by running running 4 different verifiers that were implemented by four different developers in 4 different programming languages (C, Rust, Python, and Java). There are at least 13 different Metamath verifiers, so a few more could be added if desired. The underlying Metamath language is extremely simple, too, so a verifier can be written in only a few hundred lines of code (reducing the risk of error in any one of the verifiers). There's evidence that N-version programming doesn't reduce errors as quickly as if errors were independent (see Knight and Leveson's paper), but even so, it's still quite difficult to slip by that many independent verifiers. In the long term, proof verifiers can be proven correct. It's hard to prove large programs correct, but you only need to verify the verifier; there are already examples such as ivy for prover9. I can imagine that computers might someday be better at creating proofs. But that isn't necessary for computers to be useful. The main issue today is that proofs are typically not computer-verified, and computers can do that today. Many tools have managed to do well on Freek's "Formalizing 100 Theorems" challenge list at http://www.cs.ru.nl/%7Efreek/100/ http://www.cs.ru.nl/%7Efreek/100/ - and for the most part that is without a lot of investment. It's not easy to use existing tools, that's definitely true. But a big part of the problem is that there hasn't been a lot of work to use or grow them. If more work and money was invested in improving the systems for verifying proofs, and it was held in higher regard, a lot more would happen. I believe future mathematicians will view proofs unchecked by computers the same way we view alchemy today. I suspect they'll say something like, "once in a while those alchemists and pre-mathematicians happened to be correct, but of course we don't accept their work without computer verification today." I think we should be working to make that future happen sooner.

by F-0X 8y ago

moomin 8y ago

They’re not, but they’re spectacularly good at spotting dumb errors that humans are spectacularly bad at spotting. Me, I still haven’t got my head around how to prove something on a computer, but the principle is sound. Theoretically one could build the proof as some form of literate program.

chess93 8y ago
A computer just does symbolic manipulation according to a list of rules (axioms) and the human/programmer specifies which sequence of symbolic manipulations to apply and then the computer simply states whether or not the specified manipulations transform the theorem in to the truth symbol. http://us.metamath.org/mpegif/mmcomplex.html http://us.metamath.org/mpegif/mmcomplex.html (Warning: I've never actually done much of this before so some details might be wrong.)
- dwheeler 8y ago
  I have done some, thanks for pointing to that page! Here's a prettier version for most people (the "mpegif" version uses GIFs for math symbols, which works everywhere but doesn't look at nice): http://us.metamath.org/mpeuni/mmcomplex.html http://us.metamath.org/mpeuni/mmcomplex.html

adamnemecek 8y ago

You mean unlike human?

dwheeler 8y ago

> I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect computation and software is certainly not a source of perfect logic. The issue is not that computers are always perfect. The issue is that humans are far, far worse than computers at detecting errors in proofs. So-called proofs are later found to be wrong, even after lots of human peer review, and there are often doubts about published papers. If pure math is about proof (and it is), then checking proofs with only humans is unacceptable in the long term. Humans simply aren't good enough at it, and why should we make humans do a job (verifying proofs) when computers are obviously better at it? In addition, there are many mechanisms for countering computer errors that make their likelihood essentially zero. Hardware bugs happen, but executing software on multiple different computers using diverse CPUs basically makes that disappear. Software can have errors, but there are ways to counter that too. The Metamath community verifies set.mm (its main database at http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ) by running running 4 different verifiers that were implemented by four different developers in 4 different programming languages (C, Rust, Python, and Java). There are at least 13 different Metamath verifiers, so a few more could be added if desired. The underlying Metamath language is extremely simple, too, so a verifier can be written in only a few hundred lines of code (reducing the risk of error in any one of the verifiers). There's evidence that N-version programming doesn't reduce errors as quickly as if errors were independent (see Knight and Leveson's paper), but even so, it's still quite difficult to slip by that many independent verifiers. In the long term, proof verifiers can be proven correct. It's hard to prove large programs correct, but you only need to verify the verifier; there are already examples such as ivy for prover9. I can imagine that computers might someday be better at creating proofs. But that isn't necessary for computers to be useful. The main issue today is that proofs are typically not computer-verified, and computers can do that today. Many tools have managed to do well on Freek's "Formalizing 100 Theorems" challenge list at http://www.cs.ru.nl/%7Efreek/100/ http://www.cs.ru.nl/%7Efreek/100/ - and for the most part that is without a lot of investment. It's not easy to use existing tools, that's definitely true. But a big part of the problem is that there hasn't been a lot of work to use or grow them. If more work and money was invested in improving the systems for verifying proofs, and it was held in higher regard, a lot more would happen. I believe future mathematicians will view proofs unchecked by computers the same way we view alchemy today. I suspect they'll say something like, "once in a while those alchemists and pre-mathematicians happened to be correct, but of course we don't accept their work without computer verification today." I think we should be working to make that future happen sooner.