# Can an electronic computer (stochastic) simulation be used as a “formal” proof of a tedious mathematical problem?

It seems like math purely "on paper" vs. purely on a computer both have their advantages and disadvantages. However, when combined together, they seem to greatly increase the possibilities and help confirm each methods results.

Some examples:

• Computing pi to more than a few decimal places is tedious "on paper" but "cake" for a computer.

• Someone not good in math but savvy on computers can solve some math problems such as compute how many busts are possible in a $5$ card poker hand.

• Some things are too numerous for a computer to simulate such as those with an "astronomically large" number of possible states. Even something "reasonable" such as $64 \choose 32$ is almost $2$ quintillion ($2 * 10^{18}$). Too many states for a computer (and a simple algorithm) to simulate in a reasonable amount of time, thus more clever math skills (and/or some intense pruning is needed).

So this is just "background info" but here is the real question: Suppose someone (a mathematician or maybe not) comes across a substantial discovery on a computer simulation of a "mathematical process" and wants to use it as a proof. Can he/she do it or will it be "rejected" by his/her peers without a more "traditional" (formal) proof? I've seen/heard some arguments that computers may have bugs in hardware and/or software but if multiple people get the same answer on different computers using different computer languages, then that is reassuring that the matching answers are correct.

• There's a difference between a computer-assisted proof and a computer-assisted verification of a conjecture on a large number of cases. In particular, there are many notable examples of conjectures from elementary number theory with counterexamples that don't appear until you get to very large numbers. – Nick Dec 23 '14 at 1:40
• en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer – jameselmore Dec 23 '14 at 1:43
• Who are the peers in question here? – Doug Spoonwood Dec 23 '14 at 2:29
• Doug, good point. I meant the educated math community in general. Of course his "computer buddies" would give him an "atta boy". – David Dec 23 '14 at 2:41
• Also, one can argue that computers offer "extended accuracy" because they can check billions (or more) cases that would take "an eternity" to check "by hand", thus offering "proof" of some answers that may not even be attainable on paper. Computers are excellent at counting, adding, comparing, simulating, moving data... very quickly, so I feel they are an excellent tool to help with many math problems and should be at least a good starting point/adjunct for a mathematical proof, and at best, standalone proof that a solution exists for certain math problems. – David Dec 25 '14 at 15:37

If you use a computer to work through all possible cases, then I would consider this a formal proof (obviously as long as you provide the necessary code). This is still somewhat contentious---some argue that since computers can have bugs and defects, you can't ever really know if such a proof is correct. But this seems silly to me, because humans make mistakes even more frequently than computers, so you could just as easily make the argument that as long as only humans have looked at the proof, you can't be certain it is right.

This approach is becoming more accepted. Quite recently, Harald Helfgott came up with a proof of the weak Goldbach conjecture that really would not have been possible without a computer---it took about 40,000 hours of computations to finally settle the question positively. Hopefully, we will eventually obtain a proof of this theorem that does not require so much tedious calculation, but that seems very much out of reach for the near future. There are other computer-assisted proofs out there: Computer Assisted proofs apart from the 4 color theorem.

On the other hand, if you take a random sample of possible cases and verify your conjecture for those cases, then this is not a proof, regardless of how many cases you do this for. The reason for this is that, if you were to allow such a method of "proof", you could conceivably prove things which were not true. Stochastic processes can lead you very, very astray. As an example of an extreme case, there exist events that are possible, yet have 0% probability of occurring. If you were to allow stochastic proofs, you might have a special case that disproves your conjecture, but that you would have a 0% chance of ever discovering randomly.

Simulations are very, very useful for testing conjectures and providing data to formulate ideas about what might be true. However, they (much like computer-assisted proofs, unfortunately) don't give much insight into why the conjecture is true, which is really what mathematicians care about.

• Who argues that the possibility of bugs makes computer proofs inadmissible? Both of you mentioned it, but it seems like such an obviously bad argument that no one would raise it except to reject it. – Kevin Carlson Dec 23 '14 at 2:39
• Most likely there is a paper from a philosopher of mathematics arguing this stance, but I have never cared enough to search for such a beast. That said, I have certainly heard this disgruntled argument made in casual conversation. – Arseniy Sheydvasser Dec 23 '14 at 2:57
• Arseniy: Unless someone states something like "no solution exists" so then many people upon hearing this write simulation programs and one person happens to stumble upon a single solution by luck and it is captured. Then that solution can be shared with peers and confirmed as valid. So my point is even if some simulation has an astronomical # of possible states, it may only take $1$ state to prove a solution exists and that state may be found by luck or it may just be that it came early in the simulation. At that point one could stop and say "I found a solution!". Do you agree? – David Dec 23 '14 at 2:58
• @David: Oh sure, if you are just looking for an example of something, then you are free to use a stochastic process. Granted, once you have found it, then presumably you can then just check by hand that it satisfies the desired conditions, so the stochastic process wasn't directly involved in the proof, in a certain sense. – Arseniy Sheydvasser Dec 23 '14 at 3:04
• @Arseniy, one could also use a computer to find a solution and then just stop there, declaring a "winner" and letting his/her peers deal with a more formal proof. To me, if I gave someone a mathematical problem and they showed me computer code that could find an answer, that to me is proof that such an answer exists. I would not require them to go any further. – David Dec 23 '14 at 14:59