How much faith should I put in numerics? - MathOverflow [closed]

How much faith should I put in numerics?

2009-11-29T23:48:56Z

Edit: Let me summarize what this question was meant to ask. Is there a quantitative theory of "approximate" soundness? Arguments are usually either sound or unsound. This is binary. If we don't have access to a complete argument, or are unsure whether to trust parts of an argument, can we come up with a number between 0 and 1 that quantifies how sound the incomplete or untrusted argument is?

Original rambling question below:

Before getting to the question, let me first try to make a rough distinction in what I mean by numerics. There are several types, and I'll begin with what I don't mean by numerics: something like numerical integration, or numerical root finding. I consider this zeroth case uninteresting. Problems like these are completely understood. We are just using computers to do our tedious calculations for us, and I see no reason not to trust the result.

For the first type, I'm thinking of large complex calculations such as those used in the four color theorem, or the recent proof that checkers is a draw, or maybe the recent work on the character table for split E₈. Here there are just a finite number of cases to be checked, but the computation itself is extremely elaborate just to compute about one bit of information (in the first two cases). For these types of problems, I'm imagining that there is no known way to generate a certificate that would reduce checking the validity of the calculation to an instance of case 0 numerics.

For the second type, consider numerics of the following flavor. In this scenario, my friend Bernhard has a conjecture that all of the infinitely many non-trivial zeros of a certain function lie on a certain line in the complex plane. Unfortunately, I'm not as good as Bernhard, and I don't understand his insight in proposing the conjecture. Lacking his intuition, and in lieu of a proof, I decide to numerically test the conjecture. I find that the first 10¹⁰ zeros (say) all line on the correct line.

Now I can start to get to the question. First of all, there is a fuzzy line between case 0 and case 1. Is there a way to make this line more precise?

Next, can we make precise the notion of "trusting" large calculations of the type 1 variety? How much should we trust them? Also, these types of calculations can be very unsatisfying if they don't lead you to a principle which explains why the answer is what it is. Is there a way to make this notion precise as well? Suppose that the proof of the four color theorem could be reduced to checking only 31 cases, instead of several hundred, but a computer was still necessary. Would we consider this a "good" proof? I would like to try to quantify this.

Finally, consider case 2. Have we really given any support at all to the conjecture if we've left an infinite number of cases unchecked? I'm tempted to answer a knee-jerk "No!" to this, especially in light of things like the disproof of the Mertens conjecture or Skewes' number. But it certainly feels like we've made it more plausible than if we hadn't checked those cases. I'm afraid we might have to resort to Bayesian degrees of belief here, but is there another answer?

Answer by Harrison Brown for How much faith should I put in numerics?

2009-11-30T01:50:38Z

Doron Zeilberger once described the proof of the 4CT, and other examples like Kepler's conjecture, as "one-line proof[s] modulo details," which is catchy (although I'm not sure entirely correct).

I think I disagree with your statement that "there's no way to reduce checking the validity... to case 0 numerics," although it's for what are probably overly nitpicky reasons. If you believe (or check!) the correctness of the source code, then we only have to trust that the computer's shifting bits around correctly! Sure, something could go wrong with the hardware or a lower level of the software, but this is a small probability, and if you rerun the computation on different machines at different times, it becomes vanishingly small.

So in case 1 scenarios, we've changed the problem from "trusting that an informal argument that looks like it can be formalized can be formalized" -- which is what we implicitly do when we read a mathematical "proof" to see if it is "correct" -- to "trusting that a specific formal process checks for a property that we describe sort-of-informally to other humans." This is a different question, to be sure, but I put my faith in the ability of other people to make rigorous description of processes I only understand murkily at best all the time -- for instance, as I write this, I trust (for the most part) that Firefox won't crash when I hit "Post Your Answer," that my Linux OS won't drop my wireless connection if I move my cursor too fast, that the systems my bank uses to store information won't arbitrarily take away all my money, etc.

Is my trust in these things misplaced? Occasionally. (Firefox, I'm looking at you. Don't crash! I spent too long writing this!) But these are much, much more complex problems than the simple ones in 4CT or Kepler, and when they do fail, it's usually pretty obvious. Furthermore, if an algorithm to prove 4CT or Kepler or that Checkers is a draw is at all well-designed, it can be split into "subroutines," whose correctness you can often check easily or even rigorously prove. (Again there's the problem of making sure that the algorithm's implemented correctly, but there are people who do this on a much harder scale for a living, so one hopes that we can convince ourselves that it is.) So, I think that, at least as they exist today, computer-aided proofs are still mostly just doing our tedious calculations for us.

Answer by Steve Flammia for How much faith should I put in numerics?

2009-11-30T02:45:34Z

It's pretty clear that I didn't do a good job asking this question, because it seems I'm confusing people. Let me offer a more detailed example which tries to constructively answer this question.

Consider the notion of a probabilistically checkable proof (PCP). In this setting, we can take a formalized argument and process it into a new argument whereby we only need to check a few bits of the proof to be sure with high probability that the argument is correct. One answer that I would find very satisfying, would be if there were some way we could make this construction completely canonical, so that there would be a clear notion of "how much" you need to process an argument before you accept it's claim with probability 1-ε. Then, I'm imagining that we could compare two different proofs of the same theorem by asking how much do we have to process them to get the same confidence 1-ε. Presumably this amount of processing would make some proofs more "believable" than others with the same resources.

I hope this starts to get to the heart of what I was trying to ask.