6 ms·

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 pro

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)
    - 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.
ctkrohn 14y ago
Terence Tao, one of the preeminent mathematicians working today, had a pretty good post on this exact question: http://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/ http://terrytao.wordpress.com/career-advice/there%E2%80%99s-...
- kruipen 14y ago
  Good read. You could change a few phrases and make it a post about learning programming rather than mathematics.
DanBC 14y ago
> Wait, so you're saying it's easier for humans to prove complex theorems than computers? Computer proofs tend to be brute force. For example: Are all games of Freecell winnable? But a brute force run of all Freecell games just tells us that all but one game is winnable, but tells us nothing about what's happening or why.
- njs12345 14y ago
  That's not true for proofs in assistants like Coq, which work by generating a program whose type can be checked to verify the statement in question.
dalke 14y ago
It's absolutely easier for humans to prove complex theorems than it is to encode it on a computer. Consider if your computer proof system only knows about finite numbers, when your proof deals with transfinite numbers. (There is a one-to-one mapping from each integer to each rational fraction, but there no such mapping exists from the integers to the reals, showing that size of the set of reals is fundamentally larger than the size of the set of integers, despite both being "infinite" in size. -- there is more than one type of infinity.) How do you encode that information Complicated theorems, like the four-color theorem, are different point. Note there though that the original proof of the four-color theorem, which was based on a computer enumeration, was not convincing to many mathematicians when it first came out, in part because it wasn't feasible to verify manually. Researching now, I see that a proof verified by Coq now exists, which I think reduces the amount of distrust. Yes, mathematicians "come to a consensus." And they make mistakes. Proofs are sometimes believed to be correct for several decades before being shown to be incorrect, though for important proofs - proofs that others depend on - that's extremely rare. But it isn't super handwavy. They've developed processes over time to help identify flaws. This link outlined a few of them: many people work in the same area, so they can cross-check, and workshops and other meetings serve as a way to spread knowledge and get feedback. Note how it will be a couple of years before the proof is published. If there's a missing crucial aspect, then that may reveal new types of math. Consider the work of Cantor. Quoting Wikipedia, it was "so counter-intuitive—even shocking—that it encountered resistance from mathematical contemporaries such as Leopold Kronecker and [others], while Ludwig Wittgenstein raised philosophical objections. Some Christian theologians (particularly neo-Scholastics) saw Cantor's work as a challenge to the uniqueness of the absolute infinity in the nature of God ... The objections to his work were occasionally fierce: Poincaré referred to Cantor's ideas as a "grave disease" infecting the discipline of mathematics, and Kronecker's public opposition and personal attacks included describing Cantor as a "scientific charlatan", a "renegade" and a "corrupter of youth."" Nowadays, Cantor's work is considered the origin for set theory. Part of the training in math is to make those "semantic things" well-defined. If you go further into the philosophy involved, then you start dealing with formalism, where everything is reduced to symbols manipulated by a grammar (hence how Stephenson's 'Anathem' refers to computers as 'syntactic devices'), and with Zermelo–Fraenkel set theory, which is one of the most common foundations of mathematics. However, then you have things like the continuum hypothesis and the axiom of choice which are not part of the the ZF set theory, leading to ZFC set theory. And at this point I'm well beyond what I know about the philosophy of mathematics. Suffice it to say that a full formalist description of a theorem, such that it can be reduced to a machine proof, is hard. Take a look at "Principia Mathematica" by Whitehead and Russell. Among other things, it used logic to show that 1+1=2. (See the end of the proof at http://en.wikipedia.org/wiki/File:Principia_Mathematica_theorem_54-43.png http://en.wikipedia.org/wiki/File:Principia_Mathematica_theo... - "The above proposition is occasionally useful.") That might give you a idea of what the effort looks like.
duaneb 14y ago
I suspect that Godels incompleteness theorems may imply that no single algorithm can solve all proofs. This is actually the basis for Penrose's argument that the mind is non-deterministic, though his argument is deeply flawed.
- leephillips 14y ago
  Penrose's argument, if I remember correctly, is not that the mind is necessarily non-deterministic, but that it is not equivalent to an algorithm - that you can never program a computer to create a mind. It might also be non-deterministic, but that is not exactly the same thing. His evidence for this is indeed that we can "know" the truth of theorems whose proof can not be reduced to an algorithm.
  - duaneb 14y ago
    Wouldn't finite, deterministic systems necessarily be able to be modeled by an algorithm? Either the human mind is infinite in some way, non-deterministic, or it must be able to be modeled by an algorithm. NB I am a programmer and very weak in theory.
    - leephillips 14y ago
      There is no algorithm that can determine the truth of any proposition in arithmetic (for example). It is impossible, in principle, to construct such an algorithm. But given any proposition in arithmetic, the mind can decide its truth value. It is in this sense that Penrose claims the mind can not be modeled by a computer program. It may seem odd now, but at the time there was still a school of artificial intelligence that assumed that a big computer running a really sophisticated program could be equivalent to a human mind. Penrose was trying to show that this idea is a non-starter.
      - hackinthebochs 14y ago
        >There is no algorithm that can determine the truth of any proposition in arithmetic (for example). Currently, yes. But I don't see that this is necessarily true. Why do you think it is?
shou4577 14y ago
Yes, it's much easier for humans to prove complex theorems than computers. Just as it is much easier for humans to build complex programs than computers. Often times, a proof is (much) more complicated than just mixing theorems A, B, and C together to get result D. Many times proofs will require developing entirely new mathematical structures, or can be done only in steps. As an example, a friend of mine just proved a great theorem about whether or not Hessenberg varieties can be paved by affines. Ignoring what this actually means, the proof involved firstly recognizing that a Hessenberg variety actually fits within a spectrum - it is somehow "between" other types of well- (or better-) understood varieties. These are paved by affines in (somewhat) obvious ways, and so it is natural to try to use the "between-ness" of the Hessenberg variety to construct a "between-ish" paving. This isn't a proof, but it is a direction (one that turned out to be fruitful). It would be very hard for a computer to have made this intuitive leap. And it almost works. Except now you can't reduce things like you would like, and you need to construct multi-level fiber bundles in order to get the triviality that you want. And wait - this only works if the Hessenberg variety that we started with has such-and-such property. So she's reduced the problem to a simpler problem. How does she know it is simpler? Intuition. A computer would have a very hard time recognizing whether or not this is actually simpler (even if it could get there). It turns out that this property holds when our Hessenberg variety is constructed from an element whose semisimple part under the Jordan decomposition is regular. So she has proved it for a huge class of varieties, but not all. Such a partial result would also be very difficult for a computer, since it isn't exactly what she set out to do. She's only partly there. But even this part is huge. And there isn't anything hand-wavy about her argument, either. It's perfectly grounded in well-established theorems, all of which she understands the proof for. It's just that the original concept was shakey - the "between-ness". She had to work to ground it. It would have been exceptionally hard for a computer to make several of the intuitive leaps necessary to come up with the ideas for the proof in the first place.
- deleted 14y ago
  [deleted]
- apl 14y ago
  I assume that he was going for something different, though; namely, that it's nuts that verifying proofs is simpler for humans than it is for machines.
joshmaker 14y ago
Computers may not be able to solve proofs, but they can help. In fact, there is a BOINC project aimed at finding triples for the ABC conjecture: http://en.wikipedia.org/wiki/ABC@home http://en.wikipedia.org/wiki/ABC@home
Camillo 14y ago
Honestly, you sound more like a "non-science" person there. Did you think many branches of science have an epistemology founded on automatic computation? Think again!

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)
  - 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.

ctkrohn 14y ago

Terence Tao, one of the preeminent mathematicians working today, had a pretty good post on this exact question: http://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/ http://terrytao.wordpress.com/career-advice/there%E2%80%99s-...

kruipen 14y ago
Good read. You could change a few phrases and make it a post about learning programming rather than mathematics.

DanBC 14y ago

> Wait, so you're saying it's easier for humans to prove complex theorems than computers? Computer proofs tend to be brute force. For example: Are all games of Freecell winnable? But a brute force run of all Freecell games just tells us that all but one game is winnable, but tells us nothing about what's happening or why.

njs12345 14y ago
That's not true for proofs in assistants like Coq, which work by generating a program whose type can be checked to verify the statement in question.

dalke 14y ago

It's absolutely easier for humans to prove complex theorems than it is to encode it on a computer. Consider if your computer proof system only knows about finite numbers, when your proof deals with transfinite numbers. (There is a one-to-one mapping from each integer to each rational fraction, but there no such mapping exists from the integers to the reals, showing that size of the set of reals is fundamentally larger than the size of the set of integers, despite both being "infinite" in size. -- there is more than one type of infinity.) How do you encode that information Complicated theorems, like the four-color theorem, are different point. Note there though that the original proof of the four-color theorem, which was based on a computer enumeration, was not convincing to many mathematicians when it first came out, in part because it wasn't feasible to verify manually. Researching now, I see that a proof verified by Coq now exists, which I think reduces the amount of distrust. Yes, mathematicians "come to a consensus." And they make mistakes. Proofs are sometimes believed to be correct for several decades before being shown to be incorrect, though for important proofs - proofs that others depend on - that's extremely rare. But it isn't super handwavy. They've developed processes over time to help identify flaws. This link outlined a few of them: many people work in the same area, so they can cross-check, and workshops and other meetings serve as a way to spread knowledge and get feedback. Note how it will be a couple of years before the proof is published. If there's a missing crucial aspect, then that may reveal new types of math. Consider the work of Cantor. Quoting Wikipedia, it was "so counter-intuitive—even shocking—that it encountered resistance from mathematical contemporaries such as Leopold Kronecker and [others], while Ludwig Wittgenstein raised philosophical objections. Some Christian theologians (particularly neo-Scholastics) saw Cantor's work as a challenge to the uniqueness of the absolute infinity in the nature of God ... The objections to his work were occasionally fierce: Poincaré referred to Cantor's ideas as a "grave disease" infecting the discipline of mathematics, and Kronecker's public opposition and personal attacks included describing Cantor as a "scientific charlatan", a "renegade" and a "corrupter of youth."" Nowadays, Cantor's work is considered the origin for set theory. Part of the training in math is to make those "semantic things" well-defined. If you go further into the philosophy involved, then you start dealing with formalism, where everything is reduced to symbols manipulated by a grammar (hence how Stephenson's 'Anathem' refers to computers as 'syntactic devices'), and with Zermelo–Fraenkel set theory, which is one of the most common foundations of mathematics. However, then you have things like the continuum hypothesis and the axiom of choice which are not part of the the ZF set theory, leading to ZFC set theory. And at this point I'm well beyond what I know about the philosophy of mathematics. Suffice it to say that a full formalist description of a theorem, such that it can be reduced to a machine proof, is hard. Take a look at "Principia Mathematica" by Whitehead and Russell. Among other things, it used logic to show that 1+1=2. (See the end of the proof at http://en.wikipedia.org/wiki/File:Principia_Mathematica_theorem_54-43.png http://en.wikipedia.org/wiki/File:Principia_Mathematica_theo... - "The above proposition is occasionally useful.") That might give you a idea of what the effort looks like.

duaneb 14y ago

I suspect that Godels incompleteness theorems may imply that no single algorithm can solve all proofs. This is actually the basis for Penrose's argument that the mind is non-deterministic, though his argument is deeply flawed.

leephillips 14y ago
Penrose's argument, if I remember correctly, is not that the mind is necessarily non-deterministic, but that it is not equivalent to an algorithm - that you can never program a computer to create a mind. It might also be non-deterministic, but that is not exactly the same thing. His evidence for this is indeed that we can "know" the truth of theorems whose proof can not be reduced to an algorithm.
- duaneb 14y ago
  Wouldn't finite, deterministic systems necessarily be able to be modeled by an algorithm? Either the human mind is infinite in some way, non-deterministic, or it must be able to be modeled by an algorithm. NB I am a programmer and very weak in theory.
  - leephillips 14y ago
    There is no algorithm that can determine the truth of any proposition in arithmetic (for example). It is impossible, in principle, to construct such an algorithm. But given any proposition in arithmetic, the mind can decide its truth value. It is in this sense that Penrose claims the mind can not be modeled by a computer program. It may seem odd now, but at the time there was still a school of artificial intelligence that assumed that a big computer running a really sophisticated program could be equivalent to a human mind. Penrose was trying to show that this idea is a non-starter.
    - hackinthebochs 14y ago
      >There is no algorithm that can determine the truth of any proposition in arithmetic (for example). Currently, yes. But I don't see that this is necessarily true. Why do you think it is?

shou4577 14y ago

Yes, it's much easier for humans to prove complex theorems than computers. Just as it is much easier for humans to build complex programs than computers. Often times, a proof is (much) more complicated than just mixing theorems A, B, and C together to get result D. Many times proofs will require developing entirely new mathematical structures, or can be done only in steps. As an example, a friend of mine just proved a great theorem about whether or not Hessenberg varieties can be paved by affines. Ignoring what this actually means, the proof involved firstly recognizing that a Hessenberg variety actually fits within a spectrum - it is somehow "between" other types of well- (or better-) understood varieties. These are paved by affines in (somewhat) obvious ways, and so it is natural to try to use the "between-ness" of the Hessenberg variety to construct a "between-ish" paving. This isn't a proof, but it is a direction (one that turned out to be fruitful). It would be very hard for a computer to have made this intuitive leap. And it almost works. Except now you can't reduce things like you would like, and you need to construct multi-level fiber bundles in order to get the triviality that you want. And wait - this only works if the Hessenberg variety that we started with has such-and-such property. So she's reduced the problem to a simpler problem. How does she know it is simpler? Intuition. A computer would have a very hard time recognizing whether or not this is actually simpler (even if it could get there). It turns out that this property holds when our Hessenberg variety is constructed from an element whose semisimple part under the Jordan decomposition is regular. So she has proved it for a huge class of varieties, but not all. Such a partial result would also be very difficult for a computer, since it isn't exactly what she set out to do. She's only partly there. But even this part is huge. And there isn't anything hand-wavy about her argument, either. It's perfectly grounded in well-established theorems, all of which she understands the proof for. It's just that the original concept was shakey - the "between-ness". She had to work to ground it. It would have been exceptionally hard for a computer to make several of the intuitive leaps necessary to come up with the ideas for the proof in the first place.

deleted 14y ago
[deleted]
apl 14y ago
I assume that he was going for something different, though; namely, that it's nuts that verifying proofs is simpler for humans than it is for machines.

joshmaker 14y ago

Computers may not be able to solve proofs, but they can help. In fact, there is a BOINC project aimed at finding triples for the ABC conjecture: http://en.wikipedia.org/wiki/ABC@home http://en.wikipedia.org/wiki/ABC@home

Camillo 14y ago

Honestly, you sound more like a "non-science" person there. Did you think many branches of science have an epistemology founded on automatic computation? Think again!