3 ms·

Assuming progress continues long enough: as proofs (and theorems) become more complex, the computational difficulty of verification, combined with the inherent

Assuming progress continues long enough: as proofs (and theorems) become more complex, the computational difficulty of verification, combined with the inherent physical impossibility of obtaining absolute certainty in the correctness of a computation will transform future mathematics into an empirical science, where mathematical hypotheses will be tested by computer, and results will be considered true only probabilistically.

colordrops 9y ago
That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach.
- pervycreeper 9y ago
  >That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach. Not what I'm saying. I would suggest that absolute certainty is impossible wrt verifying conventionally proved theorems as well.
  - colordrops 9y ago
    I think you moved the goal posts and are now talking about philosophy, not math. If you are saying all math is probabilistic even with conventional theorems, how can you predict a future of probabilistic math if it's already here?
    - pervycreeper 9y ago
      > are now talking about philosophy, not math Call it what you will. > If you are saying all math is probabilistic even with conventional theorems, how can you predict a future of probabilistic math if it's already here? One crucial difference is that our confidence level in a given proposition will be made explicit and will be quantified. I think you are misinterpreting what I'm saying as well-- the "experiments" I'm suggesting are not naive monte carlo simulations or tests of a nonexhaustive sample of special cases, but the generation of formal logical proofs (although not necessarily limited to that). The uncertainty would arise physically from the largeness of the computation, and once that barrier is crossed, it's conceivable that other (less rigorous) methods could be added to the battery of techniques as well (thereby increasing confidence). Also note that the size (amount of information) of the theorems and proofs would be large, and perhaps will surpass human comprehension, even after multiple stages of approximation and abstraction. The degree of confidence in such theorems would also be close to certainty as well. No human readable proofs would be harmed in the process, except for the false ones!
      - colordrops 9y ago
        I assume (perhaps incorrectly) that the terrabytes of data generated by these computational proofs are created using an algorithm that has been proven correct by a human, so I am further assuming that the potential for uncertainty you are positing comes from machine error (especially since you use the term "physical"). Are you aware of the rate of physical error in modern CPUs, memory, and storage technologies when they are arrayed in a redundant fashion? It is extremely low, and very unlikely even for a data set of this size, especially when compared to human error rates. Furthermore, were this to be replicated by someone else on another set of machines, the likelihood of the same bit flip due to physical error is so unlikely as to be astronomical in its probability.
        pervycreeper 9y ago
        >the terrabytes of data generated by these computational proofs are created using an algorithm that has been proven correct by a human Was thinking much bigger than that. Probably won't be feasible in the near future, and would of course be directed by very clever agents (mathematicians), themselves having excellent mathematical insight. >It is extremely low, and very unlikely even for a data set of this size, especially when compared to human error rates. That's the idea. Replace "practically impossible to discover or know" with knowing to an astronomically high degree of certainty. Never suggested otherwise.
- lisa_henderson 9y ago
  pervycreeper is making the point that all computers are, for practical purposes, probabilistic, since you can never know if a given result is because of a machine failure. In the normal sense of a math proof, one can not "exhaust the problem space" using a computer. Using a computer remains an empirical approach, since there is always the chance that the computer is malfunctioning.
  - colordrops 9y ago
    I don't think that's what he's saying though. He's talking about empiricism. But let's address your point. Couldn't a mind malfunction as well?
    - lou1306 9y ago
      Sure it can. As an example, d'Alembert "proved" the Fundamental Theorem of Algebra but based his work on some assumptions that made the proof incorrect. So did Euler. Correct proofs came much later thanks to Lagrange and (especially) Gauss. Problem is: a smart guy can catch a malfunctioning in another smart guy's line of reason. Can they catch an error in 200TB of proof?
      - colordrops 9y ago
        > Can they catch an error in 200TB of proof? Yes, you could either put an army of people on picking through the data, or write another software program that also picks through the data In either case, we are talking about two different things. The initial discussion was about probabilistic theorems, which is the idea of throwing a bunch of tests at a problem and getting a sense of how likely it is that the theorem is correct vs going through the entire space of a problem through brute force. Then somehow the discussion changed to whether people and computers can be trusted to not make mistakes when brute forcing the problem space, which is an entirely different subject from the topic of this post.
  - rocqua 9y ago
    The low probability of machine failure, combined with error correction means that by 4 layers of error correction, the chances of a failure (4 successive failures) are essentially nihil.

colordrops 9y ago

That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach.

pervycreeper 9y ago
>That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach. Not what I'm saying. I would suggest that absolute certainty is impossible wrt verifying conventionally proved theorems as well.
- colordrops 9y ago
  I think you moved the goal posts and are now talking about philosophy, not math. If you are saying all math is probabilistic even with conventional theorems, how can you predict a future of probabilistic math if it's already here?
  - pervycreeper 9y ago
    > are now talking about philosophy, not math Call it what you will. > If you are saying all math is probabilistic even with conventional theorems, how can you predict a future of probabilistic math if it's already here? One crucial difference is that our confidence level in a given proposition will be made explicit and will be quantified. I think you are misinterpreting what I'm saying as well-- the "experiments" I'm suggesting are not naive monte carlo simulations or tests of a nonexhaustive sample of special cases, but the generation of formal logical proofs (although not necessarily limited to that). The uncertainty would arise physically from the largeness of the computation, and once that barrier is crossed, it's conceivable that other (less rigorous) methods could be added to the battery of techniques as well (thereby increasing confidence). Also note that the size (amount of information) of the theorems and proofs would be large, and perhaps will surpass human comprehension, even after multiple stages of approximation and abstraction. The degree of confidence in such theorems would also be close to certainty as well. No human readable proofs would be harmed in the process, except for the false ones!
    - colordrops 9y ago
      I assume (perhaps incorrectly) that the terrabytes of data generated by these computational proofs are created using an algorithm that has been proven correct by a human, so I am further assuming that the potential for uncertainty you are positing comes from machine error (especially since you use the term "physical"). Are you aware of the rate of physical error in modern CPUs, memory, and storage technologies when they are arrayed in a redundant fashion? It is extremely low, and very unlikely even for a data set of this size, especially when compared to human error rates. Furthermore, were this to be replicated by someone else on another set of machines, the likelihood of the same bit flip due to physical error is so unlikely as to be astronomical in its probability.
      - pervycreeper 9y ago
        >the terrabytes of data generated by these computational proofs are created using an algorithm that has been proven correct by a human Was thinking much bigger than that. Probably won't be feasible in the near future, and would of course be directed by very clever agents (mathematicians), themselves having excellent mathematical insight. >It is extremely low, and very unlikely even for a data set of this size, especially when compared to human error rates. That's the idea. Replace "practically impossible to discover or know" with knowing to an astronomically high degree of certainty. Never suggested otherwise.
lisa_henderson 9y ago
pervycreeper is making the point that all computers are, for practical purposes, probabilistic, since you can never know if a given result is because of a machine failure. In the normal sense of a math proof, one can not "exhaust the problem space" using a computer. Using a computer remains an empirical approach, since there is always the chance that the computer is malfunctioning.
- colordrops 9y ago
  I don't think that's what he's saying though. He's talking about empiricism. But let's address your point. Couldn't a mind malfunction as well?
  - lou1306 9y ago
    Sure it can. As an example, d'Alembert "proved" the Fundamental Theorem of Algebra but based his work on some assumptions that made the proof incorrect. So did Euler. Correct proofs came much later thanks to Lagrange and (especially) Gauss. Problem is: a smart guy can catch a malfunctioning in another smart guy's line of reason. Can they catch an error in 200TB of proof?
    - colordrops 9y ago
      > Can they catch an error in 200TB of proof? Yes, you could either put an army of people on picking through the data, or write another software program that also picks through the data In either case, we are talking about two different things. The initial discussion was about probabilistic theorems, which is the idea of throwing a bunch of tests at a problem and getting a sense of how likely it is that the theorem is correct vs going through the entire space of a problem through brute force. Then somehow the discussion changed to whether people and computers can be trusted to not make mistakes when brute forcing the problem space, which is an entirely different subject from the topic of this post.
- rocqua 9y ago
  The low probability of machine failure, combined with error correction means that by 4 layers of error correction, the chances of a failure (4 successive failures) are essentially nihil.