8 ms·

Would it be possible to use proof assistants like Coq [1] to verify this kind of proofs ? If not, does anyone know why ? [1] http://en.wikipedia.org/wiki/Coq h

Would it be possible to use proof assistants like Coq [1] to verify this kind of proofs ? If not, does anyone know why ? [1] http://en.wikipedia.org/wiki/Coq http://en.wikipedia.org/wiki/Coq

cperciva 14y ago
Proofs at this level are nowhere near formal enough for existing mechanical tools to understand. I've seen researchers cite "translated proof X into an automatically-verifiable form" as a major achievement -- even for very simple proofs.
- kvb 14y ago
  This seems overly pessimistic. I'm sure it'd take a lot of work, but consider results like Gonthier's proof of the Odd Order Theorem (see http://research.microsoft.com/en-us/news/features/gonthierproof-101112.aspx http://research.microsoft.com/en-us/news/features/gonthierpr...), which formalized a book-length proof.
- makmanalp 14y ago
  Non-math person here. Wait, so you're saying it's easier for humans to prove complex theorems than computers? That's nuts. 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"? Ugh! What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions? When you describe a proof with words like you say, aren't there quibbles over semantic things? But I thought the whole point of a proof was that you leave nothing to semantics. Everything logically follows from each other. I thought the main issue with proofs systems was that encoding the concepts into code was tedious. 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? Like a package manager with proof-libraries? Or is this an issue with the expression power of proofs languages?
  - impendia 14y ago
    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)
Darmani 14y ago
Another famous theorem which is being formalized with a proof assistant is the Kepler Conjecture. It's less than half the size of the ABC Conjecture, with 250 pages of much more elementary mathematics, but the leader estimates it will take 20 years to complete. http://en.wikipedia.org/wiki/Kepler_conjecture#A_formal_proof http://en.wikipedia.org/wiki/Kepler_conjecture#A_formal_proo...

Would it be possible to use proof assistants like Coq [1] to verify this kind of proofs ? If not, does anyone know why ? [1] http://en.wikipedia.org/wiki/Coq http://en.wikipedia.org/wiki/Coq

cperciva 14y ago

Proofs at this level are nowhere near formal enough for existing mechanical tools to understand. I've seen researchers cite "translated proof X into an automatically-verifiable form" as a major achievement -- even for very simple proofs.

kvb 14y ago
This seems overly pessimistic. I'm sure it'd take a lot of work, but consider results like Gonthier's proof of the Odd Order Theorem (see http://research.microsoft.com/en-us/news/features/gonthierproof-101112.aspx http://research.microsoft.com/en-us/news/features/gonthierpr...), which formalized a book-length proof.
makmanalp 14y ago
Non-math person here. Wait, so you're saying it's easier for humans to prove complex theorems than computers? That's nuts. 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"? Ugh! What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions? When you describe a proof with words like you say, aren't there quibbles over semantic things? But I thought the whole point of a proof was that you leave nothing to semantics. Everything logically follows from each other. I thought the main issue with proofs systems was that encoding the concepts into code was tedious. 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? Like a package manager with proof-libraries? Or is this an issue with the expression power of proofs languages?
- impendia 14y ago
  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)

Darmani 14y ago

Another famous theorem which is being formalized with a proof assistant is the Kepler Conjecture. It's less than half the size of the ABC Conjecture, with 250 pages of much more elementary mathematics, but the leader estimates it will take 20 years to complete. http://en.wikipedia.org/wiki/Kepler_conjecture#A_formal_proof http://en.wikipedia.org/wiki/Kepler_conjecture#A_formal_proo...