Is the mathematical avant-garde getting so abstruse that it stretches the limits of the human mind? Is it dangerous when a science becomes entirely dependent upon the calculations of computers? Here's Sharon Begley in the WSJ:
Mathematicians have become increasingly vexed that some statements about numbers cannot be proved by humans. Worse, the proofs that computers do are so long and complicated that no one can say for sure that the statement being proved really is true, says Prof. Davies.
Two recent computer-aided proofs have this problem. One proved that to color any assembly of shapes, such as a map or a tiled floor, so that no adjoining shapes have the same color, you need only four colors. It's called the four-color theorem. Another proved that to pack the most spheres in a big box, arrange them like oranges in a crate with oranges in each upper layer resting on the dimple formed by four oranges beneath them. A third proof, only partially complete, will likely run to 10,000 pages if it is ever written down in full, says Prof. Davies, "and would not be comprehensible to any single individual."
No one has been able to check every line of these three proofs, as your 7th grade geometry teacher did. And the fact that a computer did them robs mathematicians of the joy of understanding how the necessary insight came about; the silicon ain't talking. There will be more and more proofs that no human mind will be able to follow. As mathematicians try to understand the language of Galileo's God, they may never be sure they have read it right.
I'm not too worried about the de-humanization of math. For one thing, it's not as if you can google an answer to the "four-color theorem". Mathematicians still have to design the computer program, which requires a subtle understanding of the problem they are trying to solve. Secondly, I see the increasing reliance on computers as an example of comparative advantage. We now know that the brain has very real cognitive limitations, especially when it comes to processing large amounts of information, like big numbers and long logic chains. (See George Miller, and "The Magical Number Seven".) Given these neural constraints, it only makes sense to outsource to microchips the sort of calculations that we can't do. Our comparative advantage is our imagination.
- Log in to post comments
I find it interesting that the quoted article refers to the four-color theorem as a "recent computer-aided proof". I didn't realize that "recent" meant 30 years ago.
By the way, I was at the University of Illinois at the time and attended Appel's presentation on the proof at Altgeld Hall.
Exactly. We can't see beyond red or violet, which means we can't see much of anything, but we've built doohickies to do that impossible work for us. Oh no, humans are not supermen!
"I find it interesting that the quoted article refers to the four-color theorem as a "recent computer-aided proof". I didn't realize that "recent" meant 30 years ago."
Given that we have been doing serious maths for at least 3500 years and the concept of mathematical proof is at least 2500 years old "30 yeras ago" is recent!
I wish that I could share your optimism about the dehumanization of math... It's not that I actually care whether future math is done by humans or computers, but I just don't think there will be much of a role for "human insight" in future mathematical advances. It's also unlikely that humans will continue to be involved in building the "proof programs" you mention; as computing power increases, brute force approaches to proofs will become more feasible.
Very interesting stuff!
" I just don't think there will be much of a role for "human insight" in future mathematical advances."
- This sounds so 1970's.
The 4 color proof is actually somewhat simple conceptually, just a mess of details - letting a computer check them is a good thing - the program is what then has to be "proved". Everything is actually easier to understand this way, and the nature of the computing device is just another "theorem" to be used - one which can check things with better than human accuracy.
If only it were true that shortly we would have programs that churn out proofs that we care about, then people could start looking for more interesting problems. I would love to see the day when computer "insight" got within continents of human insight.
Markk, I think we are using "insight" differently.
What I mean by "insight" is "a form of problem solving characterized by sudden onset or emotional intensity." If computers are performing the proofs, then, there will be little "human insight" involved in the proof making process. That was my (simple) point.
In contrast, your view of human involvement in future mathmeatics seems to be limited to "picking out those computer-generated proofs that people care about." That isn't necessarily an insightful process.
In 2004 I have given graph-theoretic non-computer proof of the four color theorem. It is based on spiral chain coloring of the maximal planar graphs. I can only quit in the search of non-computer proof if someone shows that there exists no non-computer proof of 4CT, Kepler Conjecture etc.
Cahit