Here is the quote I wish to ask about:
"I speculate that similar developments will occur elsewhere in mathematics, and will 'trivialize' large parts of mathematics, by reducing mathematical truths to routine, albeit possibly very long, and exorbitantly expensive to check, 'proof certificates'. These proof certificates would also enable us, by plugging in random values, to assert 'probable truth'.
taken from Zeilberger, Theorems for a Price: Tomorrow’s Semi-Rigorous Mathematical Culture.
At this point in my education (meaning that I very well may see my opinion change in the future), most of the predictions made in that paper seem brash, with all due respect. When I say this I refer to the mathematical predictions, rather than the political remarks on budgets, cost of proving theorems, etc. on which I do have some things to say, but they are for a different stack exchange site if for any.
It occurs to me that there should be an abundance of examples of a proposition that is true "99% of the time" or that has "probable truth", but fails to be true. As an aside, I can hardly fathom how "99% truth" can be precised for "wider classes of identities, and perhaps even other kinds of classes of theorems". Some immediate ones (in the sense that they are quantifiably ".99 correct", not to say that it was easy to discover them) present themselves, in the form of close calls like $$\sum_{n=1}^{\infty} \lfloor n\cdot e^{\frac{\pi}3\sqrt{163}}\rfloor 2^{-n}\stackrel{?}{=}1280640$$
when the value is actually $\frac{467807924713440738696537864469}{ 935615849440640907310521750000}\pi$, which "only" differs in the billionths. Indeed discussion similar to what I ask can be found here, here, here and here.
Apart from choosing nice examples though, another counterargument might be to address just how solid the "proof certificates" claim is. What's interesting is that Zeilberger et. al. have shown that this can be done for statements that consist of a certain hypergeometric identitiy. Therefore, it doesn't seem too far out of orbit to suggest that "truth certificates" could be found for a wide class of statements or conjectures, and this constitutes a part of my question. The second part is to ask just how wide can these go.
Putting it together: Aren't there identifiable obstructions in the task of finding a truth certificate for a given conjecture? Conversely, what about the cases exposed by Zeilberger made it possible to find them?.
For the first question, the only answer I can give myself at the moment is the ubiquitous, and for me majoritarily mystical not having studied logic, decidability. For the last part obviously I mean reasons other than the fact that they were found i.e. can, or has, the study be generalized in some way.
I hope my question is clear so far but allow me to say what I'm not asking, just to make as directed a post as possible. I do not mean to discuss:
- Romantic, if you will, counterarguments on why rigorous proof is worthy of pursuit in itself. I wholeheartedly agree on all there is to say about this.
- Practical counterarguments: "Theorem A's proof certificate would require $2^{9!}$ years to reach $6\%$ certainty.". After all, P-NP is only a problem for mortal universes.
- As I said in the beginning, social or political qualms about the "price of theorems".
Instead I mean to focus on purely mathematical or more precisely logical, barriers to this proof certificate scheme. Ironically, it sort of sounds like I'm asking how to rigorously prove that we must use rigorous proof.
P.S. I'll also appreciate references aplenty.
