[lisa_henderson]

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.

[rocqua]

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]

And furthermore, you could run it on different machines and have humans verify the results. In any case I'd trust the machines more than a human mind when it comes to consistency, and we already trust human minds with proofs.

[CJefferson]

In my experience, when a computer proof disagrees with a person proof, it's more likely the person was wrong, rather than the computer (along with the computer's programmer and hardware of course).

[colordrops]

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]

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]

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