3 ms·

> Of course! If proving theorems could be readily automated, this would have been done already. It doesn't need to create the proof, just validate it. See P v

by mbell 14y ago

> Of course! If proving theorems could be readily automated, this would have been done already. It doesn't need to create the proof, just validate it. See P vs NP.

Someone 14y ago
To have an automated proof checker validate a proof, someone would have to lay out every single step in the proof in enough detail for the verifier to do its work. With current verifiers, that means 'in painstaking detail'. Only highly educated and motivated people can do that, it takes ages, and it is not very rewarding (neither financially nor otherwise). Because of that, volunteers are hard found. In some sense we won't really know whether a proof is rock-solid until we have run it through a verifier, using a proven-correct verifier on proven-correct hardware. If theorem provers grow to be more easy to use, we may require proofs to be verified, but we aren't there yet by a wide stretch. For an idea about how hard this can be, check out http://www.cs.ru.nl/~freek/comparison/comparison.pdf: http://www.cs.ru.nl/~freek/comparison/comparison.pdf: "In 1998, Tom Hales proved the Kepler Conjecture […] with a proof that is in the same category as the Four Color Theorem proof in that it relies on a large amount of computer computation. For this reason the referees of the Annals of Mathematics, where he submitted this proof, did not feel that they could check his work. And then he decided to formalize his proof to force them to admit that it was correct. He calculated that this formalization effort would take around twenty man-years" (that effort is ongoing at http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet)
- xyzzy123 14y ago
  So would it be fair to say then, that these proof checkers are missing the 'libraries' that would be needed to efficiently write verifiable proofs for modern mathematics?
  - cperciva 14y ago
    Exactly. And this is where most of the work on proof checkers is happening -- finding ways that people can input proofs in a less formal way and have automated code fill in the formal details as a first pass before running the verification.
  - makmanalp 14y ago
    Indeed! This is exactly what I was trying to say!
makmanalp 14y ago
Right, this was what I was going for. I can't imagine computers being imaginative enough for coming up with proofs, but verifying seems like it should be rather trivial since mathematical notation is already almost rigorous enough to be a programming language.
- Evbn 14y ago
  The more advanced the math gets, the more deeply ambiguous the notation gets. Everything becomes Tx, while T and x become ever more complex objects, whose definiton is implied by context.

by mbell 14y ago

> Of course! If proving theorems could be readily automated, this would have been done already. It doesn't need to create the proof, just validate it. See P vs NP.

Someone 14y ago

To have an automated proof checker validate a proof, someone would have to lay out every single step in the proof in enough detail for the verifier to do its work. With current verifiers, that means 'in painstaking detail'. Only highly educated and motivated people can do that, it takes ages, and it is not very rewarding (neither financially nor otherwise). Because of that, volunteers are hard found. In some sense we won't really know whether a proof is rock-solid until we have run it through a verifier, using a proven-correct verifier on proven-correct hardware. If theorem provers grow to be more easy to use, we may require proofs to be verified, but we aren't there yet by a wide stretch. For an idea about how hard this can be, check out http://www.cs.ru.nl/~freek/comparison/comparison.pdf: http://www.cs.ru.nl/~freek/comparison/comparison.pdf: "In 1998, Tom Hales proved the Kepler Conjecture […] with a proof that is in the same category as the Four Color Theorem proof in that it relies on a large amount of computer computation. For this reason the referees of the Annals of Mathematics, where he submitted this proof, did not feel that they could check his work. And then he decided to formalize his proof to force them to admit that it was correct. He calculated that this formalization effort would take around twenty man-years" (that effort is ongoing at http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet)

xyzzy123 14y ago
So would it be fair to say then, that these proof checkers are missing the 'libraries' that would be needed to efficiently write verifiable proofs for modern mathematics?
- cperciva 14y ago
  Exactly. And this is where most of the work on proof checkers is happening -- finding ways that people can input proofs in a less formal way and have automated code fill in the formal details as a first pass before running the verification.
- makmanalp 14y ago
  Indeed! This is exactly what I was trying to say!

makmanalp 14y ago

Right, this was what I was going for. I can't imagine computers being imaginative enough for coming up with proofs, but verifying seems like it should be rather trivial since mathematical notation is already almost rigorous enough to be a programming language.

Evbn 14y ago
The more advanced the math gets, the more deeply ambiguous the notation gets. Everything becomes Tx, while T and x become ever more complex objects, whose definiton is implied by context.