In a Los Angeles Times commentary, Margaret Wertheim writes about one of the growning problems in modern mathematics:
People are now claiming proofs for two of the most famous problems in mathematics — the Riemann Hypothesis and the Poincare Conjecture — yet it is far from easy to tell whether either claim is valid. In the first case the purported proof is so long and the mathematics so obscure no one wants to spend the time checking through its hundreds of pages for fear they may be wasting their time. In the second case, a small army of experts has spent the last two years poring over the equations and still doesn’t know whether they add up.
She claims that mathematics is evolving into a postmodern study where, according to Philip Davis, emeritus professor of mathematics at Brown University, mathematics is “a multi-semiotic enterprise” prone to ambiguity and definitional drift.
What I found interesting was this bit:
The [four-colour map] problem was first stated in 1853 and over the years a number of proofs have been given, all of which turned out to be wrong. In 1976, two mathematicians programmed a computer to exhaustively examine all the possible cases, determining that each case does indeed hold. Many mathematicians, however, have refused to accept this solution because it cannot be verified by hand. In 1996, another group came up with a different (more checkable) computer-assisted proof, and in December this new proof was verified by yet another program. Still, there are skeptics who hanker after a fully human proof.
I don’t know if I buy the postmodern angle, but I believe she’s right about the practice of mathematics changing. It seems to me that as the complexity of mathematical problems grows beyond the abilities of human minds, we are going to require computers to prove our theorems for us. My prediction: the job of mathematicians will eventually turn into proving that theorem-proving software is correct.
Ken Dyck 