That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach.
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?
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.
Not what I'm saying. I would suggest that absolute certainty is impossible wrt verifying conventionally proved theorems as well.
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!
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.