4 ms·

All I have to say is, "Incompleteness Theorem." Hilbert tried to come up with a method of generating theorems by just cranking a wheel that churns out differen

All I have to say is, "Incompleteness Theorem." Hilbert tried to come up with a method of generating theorems by just cranking a wheel that churns out different logical forms. Ends up that we still need verification to make sure that these things actually make _sense_. (Even if we have incompleteness in any logical system that contains arithmetic, we still have to figure out whether a certain logical form "makes sense" to use.)

rfergie 16y ago
I don't understand what you're trying to say here. The incompleteness theorems are a barrier to creating a "perfect" mathematician, but certainly not a barrier to creating an adequate one. Or are you trying to say that a computer would have no idea which theorems were interesting and which were dull?
btilly 16y ago
It is clear to me that you do not understand the Incompleteness theorem, the original post, or both. I am guessing both. The fact that there are results the computer can't prove is not a bar to it being useful. After all there are results we can't prove either. What was discussed was not a perfect theorem proving system. But rather a system that was good enough to be competitive with humans.
- cparedes 16y ago
  No, I think you're not granting enough charity to what I'm saying. 1. The incompleteness theorems basically say, "if you have a logical system that includes Peano arithmetic, even if the theory is consistent, it will be an incomplete system." Also, "if you're trying to show that said system is consistent within the system, then you have an inconsistent system." These statements drop the Hilbert program to a dead halt. 2. I'm not talking about a perfect theorem proving system. However, what I _am_ saying is that you still need humans to verify the results - we do have automatic theorem provers already, but we still need to make sure that the steps are logical. Not only that, but the theorem needs to connote something useful. Also, we tend to use axioms that we can't say are consistent within the system (for instance, the axiom of choice; yet, mathematicians use it like candy in order to show useful results in analysis, and weird, unintuitive results in topology [slicing a sphere and producing two spheres with the same volume.]) I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack. 3. The reason why I'm doubtful that we'd ever see such an AI for proving math statements is because the entire enterprise is still very much a creative one - you not only have to generate the logical forms somehow, but also figure out whether it gets you closer to your goal or not. I suppose you could have some sort of heuristic that could show that a generated theorem or lemma could in fact get you closer to your goal, but my god, math is filled with so many potholes and garden paths that could lead one astray. Don't get me wrong, it'd be awesome to see such a system - however, I'm very doubtful that such a system could ever be created, and if it is created, that it'd be actually useful to practicing mathematicians.
  - btilly 16y ago
    No, I think you're not granting enough charity to what I'm saying. Let's see. The incompleteness theorems basically say, "if you have a logical system that includes Peano arithmetic, even if the theory is consistent, it will be an incomplete system." Also, "if you're trying to show that said system is consistent within the system, then you have an inconsistent system." These statements drop the Hilbert program to a dead halt. Close but not quite. The incompleteness theorem says that a consistent set of axioms describes arithmetic can only be consistent if and only if it does not prove its own consistency. An inconsistent theorem proves absolutely everything. A consistent system is welcome to attempt to prove its own consistency all it likes - it will just fail. It is true that this killed Hilbert's program as originally conceived. I'm not talking about a perfect theorem proving system. However, what I _am_ saying is that you still need humans to verify the results - we do have automatic theorem provers already, but we still need to make sure that the steps are logical. At some point, I fail to see why you need the humans. What value are humans actually providing? Not only that, but the theorem needs to connote something useful. Mathematicians already have a concept of "useful" that is so far at odds with the common understanding of the term that I honestly cannot make sense of what "useful" actually means in this context. If the program is able to tackle actual difficult research problems, and has heuristics that suffice for real problems, then its notion of "useful" is probably good enough for practice. Also, we tend to use axioms that we can't say are consistent within the system (for instance, the axiom of choice; yet, mathematicians use it like candy in order to show useful results in analysis, and weird, unintuitive results in topology [slicing a sphere and producing two spheres with the same volume.]) Outside of logic, most of mathematics has agreed on the set of axioms to use. Namely ZFC. As for using axioms that are not consistent within the system, that is absolutely necessary by the incompleteness theorem. Though you picked an ironically bad example. Gödel proved that ZF is consistent if and only if ZFC is consistent, and therefore the axiom of choice does not affect the consistency of the axiom system. It might not describe the set theory we want to describe, but it does not lead to contradictions. I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack. That was one of the weaker points made. I see the value of having heuristics that can go astray. But if you've got this in a computer, hook the heuristics up to a theorem prover that can fill in the details and come up with verified theorems. And which can alternately can describe useful plans of attacks. I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack. Until people trust the computer, it absolutely needs to be double-checked. Any piece of software can have horrible bugs that are hard to find. No matter how confident its designers are, it needs verification. The reason why I'm doubtful that we'd ever see such an AI for proving math statements is because the entire enterprise is still very much a creative one - you not only have to generate the logical forms somehow, but also figure out whether it gets you closer to your goal or not. I suppose you could have some sort of heuristic that could show that a generated theorem or lemma could in fact get you closer to your goal, but my god, math is filled with so many potholes and garden paths that could lead one astray. Yes, it looks as far away from being possible now as beating Jeopardy looked back when Deep Blue beat Kasparov. Based on my experience with mathematics and computing I find myself in agreement with rjlipton that it is not impossible, and in fact I wouldn't be surprised to see it happen within 15 years. Here is an interesting back of the envelope calculation for you. A human brain has 100 billion neurons, each of which has 7000 connections, and fires about every tenth of a second. Let's suppose that emulation averages 1000 clock cycles per synapse. The result is that simulating something as complex as the human brain in real time should take on the order of 1011 * 7000 * 1000 = 71017 clock cycles per second. Watson was running at 81012 clock cycles per second. If Moore's Law continues to hold for 16 generations, which is 24 years, then a computer the size of Watson should be able to match the human brain, in real time. Once we have the hardware, I think it is only a question of time until the necessary software is available. And given the demonstrated power of statistical analysis of large data sets to real problems (think Watson, Google translate, and the like), I think we're on our way to developing appropriate software as well. Don't get me wrong, it'd be awesome to see such a system - however, I'm very doubtful that such a system could ever be created, and if it is created, that it'd be actually useful to practicing mathematicians. I think that rjlipton is a little optimistic on the time frame. But I fully expect to see it arrive in my lifetime. I have some trepidation about the inevitable economic upheaval when it does happen.

rfergie 16y ago

I don't understand what you're trying to say here. The incompleteness theorems are a barrier to creating a "perfect" mathematician, but certainly not a barrier to creating an adequate one. Or are you trying to say that a computer would have no idea which theorems were interesting and which were dull?

btilly 16y ago

It is clear to me that you do not understand the Incompleteness theorem, the original post, or both. I am guessing both. The fact that there are results the computer can't prove is not a bar to it being useful. After all there are results we can't prove either. What was discussed was not a perfect theorem proving system. But rather a system that was good enough to be competitive with humans.

cparedes 16y ago
No, I think you're not granting enough charity to what I'm saying. 1. The incompleteness theorems basically say, "if you have a logical system that includes Peano arithmetic, even if the theory is consistent, it will be an incomplete system." Also, "if you're trying to show that said system is consistent within the system, then you have an inconsistent system." These statements drop the Hilbert program to a dead halt. 2. I'm not talking about a perfect theorem proving system. However, what I _am_ saying is that you still need humans to verify the results - we do have automatic theorem provers already, but we still need to make sure that the steps are logical. Not only that, but the theorem needs to connote something useful. Also, we tend to use axioms that we can't say are consistent within the system (for instance, the axiom of choice; yet, mathematicians use it like candy in order to show useful results in analysis, and weird, unintuitive results in topology [slicing a sphere and producing two spheres with the same volume.]) I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack. 3. The reason why I'm doubtful that we'd ever see such an AI for proving math statements is because the entire enterprise is still very much a creative one - you not only have to generate the logical forms somehow, but also figure out whether it gets you closer to your goal or not. I suppose you could have some sort of heuristic that could show that a generated theorem or lemma could in fact get you closer to your goal, but my god, math is filled with so many potholes and garden paths that could lead one astray. Don't get me wrong, it'd be awesome to see such a system - however, I'm very doubtful that such a system could ever be created, and if it is created, that it'd be actually useful to practicing mathematicians.
- btilly 16y ago
  No, I think you're not granting enough charity to what I'm saying. Let's see. The incompleteness theorems basically say, "if you have a logical system that includes Peano arithmetic, even if the theory is consistent, it will be an incomplete system." Also, "if you're trying to show that said system is consistent within the system, then you have an inconsistent system." These statements drop the Hilbert program to a dead halt. Close but not quite. The incompleteness theorem says that a consistent set of axioms describes arithmetic can only be consistent if and only if it does not prove its own consistency. An inconsistent theorem proves absolutely everything. A consistent system is welcome to attempt to prove its own consistency all it likes - it will just fail. It is true that this killed Hilbert's program as originally conceived. I'm not talking about a perfect theorem proving system. However, what I _am_ saying is that you still need humans to verify the results - we do have automatic theorem provers already, but we still need to make sure that the steps are logical. At some point, I fail to see why you need the humans. What value are humans actually providing? Not only that, but the theorem needs to connote something useful. Mathematicians already have a concept of "useful" that is so far at odds with the common understanding of the term that I honestly cannot make sense of what "useful" actually means in this context. If the program is able to tackle actual difficult research problems, and has heuristics that suffice for real problems, then its notion of "useful" is probably good enough for practice. Also, we tend to use axioms that we can't say are consistent within the system (for instance, the axiom of choice; yet, mathematicians use it like candy in order to show useful results in analysis, and weird, unintuitive results in topology [slicing a sphere and producing two spheres with the same volume.]) Outside of logic, most of mathematics has agreed on the set of axioms to use. Namely ZFC. As for using axioms that are not consistent within the system, that is absolutely necessary by the incompleteness theorem. Though you picked an ironically bad example. Gödel proved that ZF is consistent if and only if ZFC is consistent, and therefore the axiom of choice does not affect the consistency of the axiom system. It might not describe the set theory we want to describe, but it does not lead to contradictions. I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack. That was one of the weaker points made. I see the value of having heuristics that can go astray. But if you've got this in a computer, hook the heuristics up to a theorem prover that can fill in the details and come up with verified theorems. And which can alternately can describe useful plans of attacks. I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack. Until people trust the computer, it absolutely needs to be double-checked. Any piece of software can have horrible bugs that are hard to find. No matter how confident its designers are, it needs verification. The reason why I'm doubtful that we'd ever see such an AI for proving math statements is because the entire enterprise is still very much a creative one - you not only have to generate the logical forms somehow, but also figure out whether it gets you closer to your goal or not. I suppose you could have some sort of heuristic that could show that a generated theorem or lemma could in fact get you closer to your goal, but my god, math is filled with so many potholes and garden paths that could lead one astray. Yes, it looks as far away from being possible now as beating Jeopardy looked back when Deep Blue beat Kasparov. Based on my experience with mathematics and computing I find myself in agreement with rjlipton that it is not impossible, and in fact I wouldn't be surprised to see it happen within 15 years. Here is an interesting back of the envelope calculation for you. A human brain has 100 billion neurons, each of which has 7000 connections, and fires about every tenth of a second. Let's suppose that emulation averages 1000 clock cycles per synapse. The result is that simulating something as complex as the human brain in real time should take on the order of 1011 * 7000 * 1000 = 71017 clock cycles per second. Watson was running at 81012 clock cycles per second. If Moore's Law continues to hold for 16 generations, which is 24 years, then a computer the size of Watson should be able to match the human brain, in real time. Once we have the hardware, I think it is only a question of time until the necessary software is available. And given the demonstrated power of statistical analysis of large data sets to real problems (think Watson, Google translate, and the like), I think we're on our way to developing appropriate software as well. Don't get me wrong, it'd be awesome to see such a system - however, I'm very doubtful that such a system could ever be created, and if it is created, that it'd be actually useful to practicing mathematicians. I think that rjlipton is a little optimistic on the time frame. But I fully expect to see it arrive in my lifetime. I have some trepidation about the inevitable economic upheaval when it does happen.