4 ms·

Math person here. >Wait, so you're saying it's easier for humans to prove complex theorems than computers? Of course! If proving theorems could be readily aut

Math person here. >Wait, so you're saying it's easier for humans to prove complex theorems than computers? Of course! If proving theorems could be readily automated, this would have been done already. Indeed, automation has succeeded for some kinds of problems (e.g. google Wilf and Zeilberger's "WZ method" in combinatorics for a particularly successful example) >Doesn't that mean that verifying proofs is then based on a super handwavy process where a bunch of researchers come to a consensus and say "yes, this is correct"? Basically, yes. >What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions? This happens surprisingly rarely. It helps that we are trained to constantly question our entrenched assumptions. >Could we maybe have a common database of well-known proofs, axioms, concepts etc, so that you wouldn't have to rewrite common ideas from scratch? Various books fill this purpose. But the problem is that theorems are difficult to encapsulate. For example, a theorem will say "Assume X, Y, and Z. Then A and B are true." and you need to use it in some situation where Z isn't true, but some appropriate variant of Z is, and any expert would know how to conclude that A and B are true. This is when the handwaviness comes in. Mistakes do happen. But surprisingly rarely.

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.
jlouis 14y ago
Let me add to this. When you try to formalize a proof in a proof assistant, then almost all of the time, you will find numerous errors in the proof. But - and this is key - these errors are usually fixable or the area is not understood well enough and requires more attention to detail. The human intuition is quite powerful.
- scotty79 14y ago
  That's similar to when you subject working software system to new batch of tests or test it in some new way. Usually a lot of previously known errors will crop up despite that the system already works mostly as intended.
Evbn 14y ago
Zeilberger has some nice examples of human error on his blog. He would love to see much more use of computer provers to clean up the errors made by human writers and readers.
pseut 14y ago
>>What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions? >This happens surprisingly rarely. It helps that we are trained to constantly question our entrenched assumptions. It also helps that finding a counterexample to a widely accepted proof tends to enhance one's career and reputation.

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.

jlouis 14y ago

Let me add to this. When you try to formalize a proof in a proof assistant, then almost all of the time, you will find numerous errors in the proof. But - and this is key - these errors are usually fixable or the area is not understood well enough and requires more attention to detail. The human intuition is quite powerful.

scotty79 14y ago
That's similar to when you subject working software system to new batch of tests or test it in some new way. Usually a lot of previously known errors will crop up despite that the system already works mostly as intended.

Evbn 14y ago

Zeilberger has some nice examples of human error on his blog. He would love to see much more use of computer provers to clean up the errors made by human writers and readers.

pseut 14y ago

>>What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions? >This happens surprisingly rarely. It helps that we are trained to constantly question our entrenched assumptions. It also helps that finding a counterexample to a widely accepted proof tends to enhance one's career and reputation.