4 ms·

What is Experimental Mathematics?

ihodes 17y ago
Another interesting mathutation article on HN... Nice. I've got to say, both in CS/hacking and math, I find myself spending a lot of time carrying out computations to get a feel for a problem. I poke around a problem until an answer begins to form in my mind - enough evidence pointing me in one direction heavily sways my opinion and even approach to solving a problem. But is computation math? I suppose it's purely semantic, but I still see a difference between hackin' away at a problem and finding an irrefutable proof of a problem; though often the former leads to the latter. As a NB, I'd like to add that Mathematica can be used to do "pure" mathematics, too.
- yters 17y ago
  Nope, computation can never be the same as math, per Godel's incompleteness theorem. Which, perchance, is also a good illustration of the difference between proof and merely cranking through a problem space.
  - iskander 17y ago
    >Nope, computation can never be the same as math, per Godel's incompleteness theorem. lolwut? (first order logic w/ addition ain't math enough for you?)
  - roundsquare 17y ago
    So, if you are going to refer to Godel's theorem, its best to explain your point. Godel's theorem is on of the most poorly understood popular ideas in mathematics and its easy to trip over (for you or the reader). I'm going to try to guess what you mean. You are trying to say that since a computer is essentially a formal system and humans are something more, we can't replace human mathematicians with computers to do the work because they won't be able to come up with new ideas outside a fixed problem space? In any event, I think you are misunderstanding @ihodes's question. The question is not "can we replace mathematicians with computers" but is more about the practice of mathematics. I.e., @ihodes is asking if the mental activity of experimenting and doing computations is conceptually similar to doing proofs.
  - Confusion 17y ago
    As iskander put somewhat less eloquently: what you say does not make any sense. Godel's incompleteness theorem places a theoretical limit on the completeness of (non-trivial) formal mathematical systems. 'Computations' take place within such formal systems and are, by definition, math. Both are subject to the consequences of Godel's theorems and you can't distinguish between them based on those theorems.
    - yters 17y ago
      Assuming math encompasses Godel's theorem, then computer science can only be a subset of math at best, since a computer can not prove Godel's theorem.
merraksh 17y ago
And even then, which do you find more convincing, the fact that there is an argument - which you have never read, and have no intention of reading - for which none of the hundred or so errors found so far have proved to be fatal, or the fact that the hypothesis has been verified computationally (and, we shall assume, with total certainty) for 10 trillion cases? What is more likely, a fatal error in the proof or a bug in the program? Proving (computationally or not) correctness of a program (or a proof) is not easy.
- Herring 17y ago
  Proofs are hard. False positives in programs are very unlikely. It's usually a matter of verifying a few examples by hand because it's really hard to have isolated false positives.
  - roundsquare 17y ago
    I don't really agree with that. Two examples come to mind: 1) Four color map theorem. I wouldn't have been horribly surprised if the code used to prove this made a mistake in 1,936 maps it had to check. Give that a second program verified it, I'd be more surprised now, but at the time, I would have been most worried about how to input the 1,936 maps. (I have no idea how this was done, if even generating them was programmatic, errors would have been less likely). 2) Automated symbolic logic programs are probably easy to make mistakes with. You need to have perfect parsing logic on the strings of each theorem and generate the new strings perfectly. I'm not saying its impossible, but mistakes are probably easy to make.
    - Herring 17y ago
      It occurs to me that the author & I are sort of making the same point: checking a bunch of points gives you a degree of confidence in the general case. I think the only way to settle it is to quantify it.

Another interesting mathutation article on HN... Nice. I've got to say, both in CS/hacking and math, I find myself spending a lot of time carrying out computations to get a feel for a problem. I poke around a problem until an answer begins to form in my mind - enough evidence pointing me in one direction heavily sways my opinion and even approach to solving a problem. But is computation math? I suppose it's purely semantic, but I still see a difference between hackin' away at a problem and finding an irrefutable proof of a problem; though often the former leads to the latter. As a NB, I'd like to add that Mathematica can be used to do "pure" mathematics, too.

yters 17y ago
Nope, computation can never be the same as math, per Godel's incompleteness theorem. Which, perchance, is also a good illustration of the difference between proof and merely cranking through a problem space.
- iskander 17y ago
  >Nope, computation can never be the same as math, per Godel's incompleteness theorem. lolwut? (first order logic w/ addition ain't math enough for you?)
- roundsquare 17y ago
  So, if you are going to refer to Godel's theorem, its best to explain your point. Godel's theorem is on of the most poorly understood popular ideas in mathematics and its easy to trip over (for you or the reader). I'm going to try to guess what you mean. You are trying to say that since a computer is essentially a formal system and humans are something more, we can't replace human mathematicians with computers to do the work because they won't be able to come up with new ideas outside a fixed problem space? In any event, I think you are misunderstanding @ihodes's question. The question is not "can we replace mathematicians with computers" but is more about the practice of mathematics. I.e., @ihodes is asking if the mental activity of experimenting and doing computations is conceptually similar to doing proofs.
- Confusion 17y ago
  As iskander put somewhat less eloquently: what you say does not make any sense. Godel's incompleteness theorem places a theoretical limit on the completeness of (non-trivial) formal mathematical systems. 'Computations' take place within such formal systems and are, by definition, math. Both are subject to the consequences of Godel's theorems and you can't distinguish between them based on those theorems.
  - yters 17y ago
    Assuming math encompasses Godel's theorem, then computer science can only be a subset of math at best, since a computer can not prove Godel's theorem.

merraksh 17y ago

And even then, which do you find more convincing, the fact that there is an argument - which you have never read, and have no intention of reading - for which none of the hundred or so errors found so far have proved to be fatal, or the fact that the hypothesis has been verified computationally (and, we shall assume, with total certainty) for 10 trillion cases? What is more likely, a fatal error in the proof or a bug in the program? Proving (computationally or not) correctness of a program (or a proof) is not easy.

Herring 17y ago
Proofs are hard. False positives in programs are very unlikely. It's usually a matter of verifying a few examples by hand because it's really hard to have isolated false positives.
- roundsquare 17y ago
  I don't really agree with that. Two examples come to mind: 1) Four color map theorem. I wouldn't have been horribly surprised if the code used to prove this made a mistake in 1,936 maps it had to check. Give that a second program verified it, I'd be more surprised now, but at the time, I would have been most worried about how to input the 1,936 maps. (I have no idea how this was done, if even generating them was programmatic, errors would have been less likely). 2) Automated symbolic logic programs are probably easy to make mistakes with. You need to have perfect parsing logic on the strings of each theorem and generate the new strings perfectly. I'm not saying its impossible, but mistakes are probably easy to make.
  - Herring 17y ago
    It occurs to me that the author & I are sort of making the same point: checking a bunch of points gives you a degree of confidence in the general case. I think the only way to settle it is to quantify it.