Comment by breadbox

13 years ago

Interesting. I had assumed at this point in time that computers were ubiquitous in math research. It's mind-boggling to me that there is still any significant level of pushback against using them. (I suppose that getting a CS-specific math degree gives one a skewed perspective on such details.)

Also, the point of not having standard programming classes leads to a lack of standards in research coding is an important one.

25 comments

breadbox

Reply
walrus  13 years ago

Computers are used in (some parts of) math for exploration, but not so much when it comes to conjectures and proofs. In fact, I would argue that making conjectures is a distinctly human activity: it requires you to decide if something is 'interesting' or not.

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.

strangestchild  13 years ago

I think this is very dependent on the area of maths. In applied mathematics, obviously simulation is of huge importance; and in very fundamental pure maths the language is close enough to formal logic to make it easier to apply computer-aided proof.

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.

lutze  13 years ago

To me, this is akin to asking "as building materials grow heavier, will cranes reign?"

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.

  • Retric  13 years ago

    Some math such as geometric proofs are still harder for many people to do on computers. There is always a cost/benefit calculation when building and learning to use tools. So, while it may seem obvious to us that software is a net win, when you don't think in those terms it's far from obvious that it is.

  • eric-hu  13 years ago

    It depends on the kind of mathematician. Can you use a computer to demonstrate Russel's paradox? Clipped from Wikipedia:

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

  • fusiongyro  13 years ago

    It probably doesn't help that we go around parroting the ludicrous notion that you don't need math to program. It can hardly be true that you need to program to do math when we've been doing math for millenia.

    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?

    • lutze  13 years ago

      No one is saying that.

      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!

      2 replies →

    • jamesrcole  13 years ago

      It's got nothing to do with need. It's whether it would be useful or not.

      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.

    • enraged_camel  13 years ago

      >>It probably doesn't help that we go around parroting the ludicrous notion that you don't need math to program.

      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.

      2 replies →

xamuel  13 years ago

Computers are ubiquitous in math research. We use LaTeX to type the research up and we email it to each other. (Ba dum ching!)

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.