As Math Grows More Complex, Will Computers Reign?
wired.com
wired.com
Also, the point of not having standard programming classes leads to a lack of standards in research coding is an important one.
On the proving side, there is some software such as Coq or Agda that provide heuristics, but you won't find the typical mathematician using them. In many proofs, things are said to be 'obvious' or 'follow clearly' from a previous statement. A mathematician (trained in the relevant area of math) can fill in those parts with their intuition, but a computer can't. That often makes a computer-readable proof prohibitively long compared to a human-readable one.
That's not to say mathematicians shouldn't learn to use that sort of software. The only way to fill in those 'obvious' or 'follows clearly' parts is to build a large library of arguments that can fill them in.
But in very pure disciplines which rely on several layers of supporting definitions and theorems, there is little to be gained from numerical computation - but huge amounts of bootstrapping are still required before the computer can prove results of its own using logical manipulation.
To take a simple example, writing a computer program capable of proving that there are infinitely many primes - without embedding so much domain knowledge in it as to render it useless - seems a pretty nontrivial task.
I am not that familiar with the field, but http://us.metamath.org/mpegif/infpnlem2.html fits on one page. If you fully expand the proofs of each subclause, I don't know how long it is, but it won't fit on a page. You will get through to the 'bloody obvious', though, with such things as http://us.metamath.org/mpegif/syl.html "if A implies B and B implies C, then A implies C", which this system proofs from http://us.metamath.org/mpegif/a1i.html "if A is true, then anything implies it" and http://us.metamath.org/mpegif/ax-mp.html "if A is true and A implies B, then B is true"
Each of these may lead to new branches of mathematics in which Euclid's theorem does not hold or only holds in a restricted way.
I am not denying that writing automated proofs is a nuisance, but you also get more in the process. For proofs like this, barely anything more, but surely, the promise is there.
Computers have always been envisioned as levers for the mind. The fact that mathematicians of all people aren't taking full advantage of that principle utterly boggles my mind too.
> Let us call a set "abnormal" if it is a member of itself, and "normal" otherwise.
> Now we consider the set of all normal sets, R. Determining whether R is normal or abnormal is impossible: If R were a normal set, it would be contained in the set of normal sets (itself), and therefore be abnormal; and if R were abnormal, it would not be contained in the set of all normal sets (itself), and therefore be normal. This leads to the conclusion that R is neither normal nor abnormal: Russell's paradox.
Russel's paradox "broke" set theory. In the century since he discovered it, category theory was introduced as a mathematical way to capture groupings in a way that set theory failed to do.
I don't see how computers can assist in this kind of mathematical research. I do believe there's lots of research of this kind too, pushing the limits of our current mathematical structures.
How long can you mock your older brother in front of your hip young friends before he decides to ignore you and go play with his own friends somewhere else?
Levers. No one said the pulley (or CAD) rendered the architect defunct, and no one is saying computers should do the same for mathematicians. We're just trying to understand this resistance to using tools to help do heavy lifting, the “human-centric bigotry” as the article puts it. Reading some of the responses here, it's probably being overstated, but even so.
And ignore you and go play somewhere else? A good number of the most influential computer scientists have actually been psychologists, not mathematicians, so the older brother needs to get the fuck over himself if that's his attitude!
I'd like to hear who you consider influential computer scientists coming from psychology. The ones I hold dear are mostly settlers from math.
If the younger brother were as wise as he thinks he is, he wouldn't need to get so worked up as to substitute profanity for an articulate argument.
Edit: As for psychologists, you're seriously telling me you never heard of Licklider? That's... astounding.
Consider programming. You don't need anything more than punch-cards to program. You don't need anything more than assembler. But higher-level languages can be useful, because they can make the task easier, give you greater leverage.
I thought the consensus was that it really depends on the type of problems one is trying to solve, and that most programmers can in fact get away with knowing little math.
I actually had a peer reviewer ask me to formalize a paper of mine in Coq, and I did so. It's a wonderful experience and it opened my eyes (thanks, reviewer) but it was only feasible in this paper's case because this paper dealt with extremely formal logical syntax. Even so, for every page of human-readable paper, the formalization had two pages of incredibly hard-to-read (and even harder to write) code. For anything more semantical, it's completely unreasonable in the short-term future.
Even if there are some branches of mathematics that will be affected by computers, at the end of the day, there will still have to be someone who does the conjecturing, someone with enough knowledge to pose the question to the computer.
Basically, you hop up a level (go meta). Instead of working with the extremely large numbers or sets, you symbolically manipulate statements about them.
I'll repeat what szany and xyzzy123 mentioned: you work at a level of abstraction where infinite data structures are represented symbolically with enough definitional scaffolding to allow proofs to go through.
In a sense, a properly typed program provides a proof of some theorem over infinite data structures. For instance, an instance of a tree (in generic Java) is usually a finite data structure, but the set of all trees representable in Java is infinite. (Handwaving begins) The types prove that certain operations can't happen, like a tree of Strings changing to a tree of Arrays by a node search algorithm, which is a proof about an infinite set.
You're assuming that computers can't handle abstractions.
How does a computer build abstractions on its own?
But it doesn't have to do that, anyway, it can provide means for users to build their own abstractions, abstractions that may be useful for them.
It's available for download at http://www.math.upenn.edu/~wilf/AeqB.html
http://www.math.upenn.edu/~wilf/AeqB.pdf
http://www.math.rutgers.edu/~zeilberg/AeqB.pdf
http://www.fmf.uni-lj.si/aeqb/AeqB.pdf
The license agreement is (copied and pasted from the download page):
Copyright 1996 by A K Peters, Ltd.
Reproduction of the downloaded version is permitted for any valid
educational purpose of an institution of learning, in which case only
the reasonable costs of reproduction may be charged. Reproduction for
profit or for any commercial purposes is strictly prohibited.Although, perhaps this is verging on philosophy: is such a process even possible? Do current (or future) computer programs involve leaps of intuition, and abstractions that cannot be mathematically codified?