Computations alone will not do, as there are many undecidable statements that are provably correct. Considering the Mathematical Universe as a fixed entity gives the working mathematician a strong drive, but one forgets that some properties require a lot of energy to find out (sometimes infinitely much, i.e. one cannot do it). Systems using formal intuitionism for computer mathematics, like Coq and Nuprl have found the right middle way. On the other hand, if intuitionism is considered as a philosophy that states that mathematics only exists in the human mind, one would limit oneself to what may be called in a couple of decades 'pre-historic' mathematics. True, the theories that can be fully run through in our mind constitutes romantic mathematics. But the expected results fully checked by computers that have been checked (by computers that have been checked)n by us will be cool mathematics.
...
Astronomy and biology have also had their romantic phase of going out in the fields and studying butterflies, plants and stars. The biologist at first could see everything with the naked eye. Then came the phase of the microscope. At present biologists use EM (electro-microscopy) or computers (the latter e.g. for gene sequencing). Very cool. The early astronomers could study the planets with the naked eye. Galileo started using a telescope and found the moons of Jupiter and mountains on the earth's moon. Nowadays there are sophisticated tools for observations from satellites. Again, very cool. Still, even today both biology and astronomy remain romantic, albeit in a different way. In a similar manner, the coolness of Computer Mathematics will have its own romantics: human cleverness combined with computer power finding new understandable results.
Wednesday, January 10, 2007
"Cool Mathematics"
From Foundations of Mathematics from the perspective of Computer Verification by Henk Barengregt:
Subscribe to:
Post Comments (Atom)
2 comments:
On the plane just now, I just read something similar (at least to the first paragraph above). It was on how King Alfred created his own literary persona in his letters and translations: 1) frequent references to his ability to remember the subjects of his writing just as they were; 2) a near-infinite field of subjects. The unspoken limitation was of course his human mental capabilities, a point discussed at length in one of his sources but ignored in his own writing.
It was the technology of literacy, argues Seth Lerer (the dude I'm now reading), that allowed Alfred's literary aspirations to migrate from the incomplete/romantic to the "cool". The idea that Alfred could keep on talking/teaching/instructing even in his absence was a defining aspect of how his kingship extended its power.
I think that lines up nicely... maybe...?
I agree, I think it does. One thing technology (computer or literary) facilitates is the use of one's brain for "more human" activities. That is, while a piece of paper is just as good (well, likely better) at remembering a phone number written on it than you are, that piece of paper can't have a conversation with the person whose number it is. That's a human task, and you really ought to be able to devote your mind to having that conversation, not remembering the number.
An interesting thing related to this is the extent to which the particular technology we elect to use affects the work we choose to do. For instance (to tie paper, computer-assisted proof, and this comment together), the Four Color Theorem talks about a particular class of graphs which, among other things, are easily and clearly represented on chalkboards. How many classes of graphs are there whose definitions are no more complex than that of planar graphs that we pay no attention to, because they don't relate to the particular tools we use on a regular basis? (I should concede that planarity is a property of our standard model of space, and so it might be quite natural to worry about classes of graphs which correspond to "reality".)
Might a similar statement be made about literature? Epic poems were, I'm told, originally memorized and performed, rather than written and read. As literacy and better writing technology developed, this form gave some way to, for instance, the novel.
Post a Comment