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 E8. 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 1010 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?

  • $\begingroup$ Please feel free to help me sharpen the phrasing of the question of the classification of numerics (including if I've omitted anything). I'll try to incorporate good suggestions into the body of the question, with reference to the original author, so that the question remains easy to read without too much cross referencing. Suggestions for retags also welcome. $\endgroup$ – Steve Flammia Nov 29 '09 at 23:49
  • 6
    $\begingroup$ I vote to close. Reason: subjective and argumentative. $\endgroup$ – S. Carnahan Nov 30 '09 at 1:29
  • 1
    $\begingroup$ I can't fit a full discussion in a comment box, but I can offer a reason. Your question carries an implicit assumption that arguments generated by humans should be trusted more than those generated by computer. I would argue that this assumption is ill-founded. For example, there is a proof of the four-color theorem that has been computer-verified from start-to-finish. I would trust this much more than, e.g., certain refereed literature using algebraic stacks. This also feeds into the troublesome issue of bias against people who practice computational mathematics and formal verification. $\endgroup$ – S. Carnahan Nov 30 '09 at 2:23
  • 2
    $\begingroup$ I think this is a great question for a discussion forum, but a lousy one for MO. So I'm with Scott on the procedural vote. If this were a discussion forum, I would engage with the question on the merits. $\endgroup$ – Theo Johnson-Freyd Nov 30 '09 at 2:42
  • 1
    $\begingroup$ Your new question doesn't seem very mathematical to me. How can you trust an argument at all if you don't have access to parts of it? In principle, those parts could hide fatal errors. (In practice, it seems to me that errors in human-written proofs tend not to be fatal, but again - not a mathematical question.) $\endgroup$ – Qiaochu Yuan Nov 30 '09 at 3:42

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.

  • $\begingroup$ I take it you are saying that the distinction between cases 0 and 1 is merely one of degree. Fair enough. One thing that I'm trying to get at with this question is, can we compute a number which says how certain we are? Some kind of confidence interval, or something? Especially if this number could be given some kind of objective meaning, as opposed to a Bayesian degree of belief. (I realize this might be impossible.) $\endgroup$ – Steve Flammia Nov 30 '09 at 2:01
  • $\begingroup$ Hmm. I suppose one could estimate the probability of a glitch that caused the computer to give the wrong output even though the software and hardware are "working," but that's for all practical purposes 0. Other than that, you're arguably asking a straight-up computer science question, which I'm pretty clueless about. $\endgroup$ – Harrison Brown Nov 30 '09 at 2:22
  • $\begingroup$ Such a computation would rely on a physical model, and this would inevitably degenerate into a Bayesian degree of belief. Let me offer a very vague notion of what I'm aiming for. Can we make our proofs "fault tolerant" in the sense that if we are unable to check certain details, we can still compute a probability that the conclusion is correct? Maybe I need to rewrite this question... $\endgroup$ – Steve Flammia Nov 30 '09 at 2:29

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.

  • $\begingroup$ Then it's not a proof, is it? $\endgroup$ – Harry Gindi Nov 30 '09 at 5:48

Not the answer you're looking for? Browse other questions tagged or ask your own question.