I always enjoy Brian Hayes’ Computing Science feature in American Scientist, but his thoughts on the real-world applicability of mathematical proof were both interestinig and laugh-out-loud funny, if you’re the sort of person to laugh out loud at angle trisection jokes and spoofs of Socratic dialog. The article also discusses the controversy over the imfamous computer-aided proof of the four-color theorem and the recent Hales proof of the Kepler conjecture. Hayes comes down on the side of computer assistance as a valid and valuable aid, not least as a tool for providing empirical data and aiding intuition. This is supported in part by a broad understanding of the point of mathematical proof:

The special status of mathematical truth, setting the discipline apart from other arts and sciences, is a notion still cherished by many mathematicians, but proof has other roles as well; it’s not just a seal of approval. David Bressoud’s book Proofs and Confirmations gives what I believe is the best-ever insider’s account of what it’s like to do mathematics. Bressoud emphasizes that the most important function of proof is not to establish that a proposition is true but to explain why it’s true. “The search for proof is the first step in the search for understanding.”

trisection of an angle is possible because it is prved by u.k.sharma in december