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.
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?
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.
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.
> 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.
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.