> I can envision an abstract of a paper, circa 2100, that reads: "We show in a certain precise sense that the Goldbach conjecture is true with probability larger than 0.99999 and that its complete truth could be determined with a budget of $10 billion." It would then be acceptable to rely on such a priced theorem, provided that the price is stated explicitly. Whenever statement A, whose price is p, and statement B, whose price is q, are used to deduce statement C, the latter becomes a priced theorem priced at p+q. If a whole chain of boring identities were to turn out to imply an interesting one, we might be tempted to redeem all these intermediate identities; however, we would not be able to buy out the whole store, and most identities would have to remain unclaimed. As absolute truth becomes more and more expensive, we would sooner or later come to grips with the fact that few nontrivial results could be known with old-fashioned certainty. Most likely, we will wind up abandoning the task of keeping track of price altogether and complete the metamorphosis to nonrigorous mathematics.
This seems quite a good prediction to me. Consider that today there exist many mathematical proofs based on heurestics and probabilities. Furthermore, while we don't assign prices to theorems, there is the fact that with the coming of Lean and Coq, we may start seeing some mathematical proofs become immensively expensive to produce and verify due to running costs. The four colour theorem is just one example.