Charlie Noback pointed me to an interesting article in the WSJ on the limits of human reasoning in Mathematics, When Number Proofs Are Done by Computer, Mightn’t Some Err?.

“If I have $15 and you have $20, and we keep tossing a coin so that you win $1 from me if it turns up heads and I win $1 from you if it lands tails, you have a reasonable chance of eventually bankrupting me and walking away with the whole $35. But your prospects are not so overwhelmingly great that I refuse to play. In fact, your probability of winning it all equals your $20 divided by the sum of our stakes ($35), or just 57%. The “gambler’s ruin” problem has entranced mathematicians since the 1800s, and at this week’s annual meetings of the American Mathematical Society and the Mathematical Association of America in New Orleans it played another role: “as a case study in the limits of proof and of machine proofs,” says mathematician Doron Zeilberger of Rutgers University. Mathematicians, to their dismay, are the first scientists to face the shattering and humbling prospect that the complexities of nature may be beyond the reach of the human mind.”

Zeilberger’s article Symbol-Crunching With the Gambler’s Ruin Problem is online along with a Maple package that automatically computes, symbolically (and numerically), statistical quantities related to the Gambler’s Ruin problem.

It’s well know that machine generated proofs are hard to understand and to check. The WSJ article has an interesting quote from an AMS article Whither Mathematics? by Brian Davies

If the goal of mathematics is understanding, then one cannot deny that computer-assisted proofs do not supply it in full measure.

Categories: Uncategorized, Related posts: • W3C issues report on uncertainty reasoning for the Web;  • An intelligent geospatial reasoning system;  • Wisdom of the Web Crowds: PageRank Explained;