6 ms·

As Math Grows More Complex, Will Computers Reign?

32 points by gtani 14y ago

breadbox 14y 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.
- lutze 14y 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 14y 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.
  - fusiongyro 14y 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?
    - enraged_camel 14y 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.
      - deleted 14y ago
        [deleted]
      - calhoun137 14y ago
        Just because something is a consensus doesn't make it true. And its not a consensus, its just the majority view that a minority of us find incredibly backwards. Just because you can get away with something doesn't mean its a good idea either. You can get away with a lot in programming, back yourself into a corner, and hack your way out, does that mean since you can get away with it that its a good idea to program like that?
    - lutze 14y 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!
      - fusiongyro 14y ago
        The problem is that these tools don't help much. In other fields, people clamor for software because software can excel at things humans are bad at: repetitive tasks, rote calculations, lots of arithmetic. The hard part of the proof is coming up with it, not checking it. And coming up with the proof requires deep insights, which means a library of proofs isn't as useful as a library of code where you can use the code without having to understand it. What we have so far is pretty good at checking proofs but very bad at coming up with them. So what you're actually engaging in here is "machine-centric bigotry"--the idea that the machine is intrinsically better at all problem solving than man, despite evidence to the contrary. 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.
  - eric-hu 14y 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.
- strangestchild 14y 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.
  - Someone 14y ago
    Nontrivial, but doable. See #11 in http://www.cs.ru.nl/~freek/100/ http://www.cs.ru.nl/~freek/100/ Also: http://us.metamath.org/mpegif/infpn.html http://us.metamath.org/mpegif/infpn.html
    - fusiongyro 14y ago
      I think it supports strangestchild's thesis that all five proofs from this page[1] would fit on a page and a half printed but the Coq proof (the only one I could find a download for from your list) is 825 lines of code. [1]: http://primes.utm.edu/notes/proofs/infinite/ http://primes.utm.edu/notes/proofs/infinite/
      - Someone 14y ago
        You can easily fit all of them on one page, as long as you build enough scaffolding theorems to get there. I am not that familiar with the field, but http://us.metamath.org/mpegif/infpnlem2.html 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 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 http://us.metamath.org/mpegif/a1i.html "if A is true, then anything implies it" and http://us.metamath.org/mpegif/ax-mp.html http://us.metamath.org/mpegif/ax-mp.html "if A is true and A implies B, then B is true"
- walrus 14y 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.
- gtani 14y ago
  Yeah, pretty fluffy article, no mention of HOL, dependent types, other camps. I was hoping to see libs like Isabelle, metaMath, Corbineau's coq lib etc mentioned
  - szany 14y ago
    There was a mention of dependent types.
  - dubya 14y ago
    Isabelle was used for the proof of the prime number theorem. The link from the article: http://repository.cmu.edu/cgi/viewcontent.cgi?article=1032&context=philosophy http://repository.cmu.edu/cgi/viewcontent.cgi?article=1032&#...
- xamuel 14y 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.
  - marchdown 14y ago
    I'm not sure that it's appropriate to ask, but I would love to see the paper.
    - xamuel 14y ago
      Here is the paper: http://arxiv.org/abs/1105.4135 http://arxiv.org/abs/1105.4135 And here is the formalization of sections 2-3 in Coq: http://www.math.osu.edu/~alexander.421/mech.txt http://www.math.osu.edu/~alexander.421/mech.txt
      - marchdown 14y ago
        Thanks.
gems 14y ago
How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers? You can't ask the computer to enumerate the solutions for you. You have to reason in a roundabout way, possibly building some abstraction. 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.
- meaty 14y ago
  That is until a computer is capable of reason, which I personally think will never happen. I'm not suggesting some other technology will not be able to reason, but it's not going to be a jumped up Turing machine.
- xyzzy123 14y ago
  > How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers? Basically, you hop up a level (go meta). Instead of working with the extremely large numbers or sets, you symbolically manipulate statements about them.
  - gems 14y ago
    Give me an example of how this is done or can be done.
    - sharkbot 14y ago
      Check out Adam Chlipala's Coq tutorial, specifically the section on infinite proofs: http://adam.chlipala.net/cpdt/html/Coinductive.html http://adam.chlipala.net/cpdt/html/Coinductive.html 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.
d4vlx 14y ago
No http://en.wikipedia.org/wiki/Betteridges_law_of_headlines http://en.wikipedia.org/wiki/Betteridges_law_of_headlines
walrus 14y ago
If you find this sort of thing interesting, you may enjoy A=B by Marko Petkovsek, Herbert Wilf, and Doron Zeilberger. (Wilf was mentioned in the article.) It's available for download at http://www.math.upenn.edu/~wilf/AeqB.html http://www.math.upenn.edu/~wilf/AeqB.html
- jonahkagan 14y ago
  Link seems to be down, but I'd be interested.
  - walrus 14y ago
    If you're still having trouble accessing it, here are direct links to the mirrors: http://www.math.upenn.edu/~wilf/AeqB.pdf http://www.math.upenn.edu/~wilf/AeqB.pdf http://www.math.rutgers.edu/~zeilberg/AeqB.pdf http://www.math.rutgers.edu/~zeilberg/AeqB.pdf http://www.fmf.uni-lj.si/aeqb/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.
- dubya 14y ago
  I would like to add that Doron Zeilberger's opinions page is very interesting: http://www.math.rutgers.edu/~zeilberg/OPINIONS.html http://www.math.rutgers.edu/~zeilberg/OPINIONS.html
fractallyte 14y ago
One of the reciprocal outcomes of this could be method(s) to mathematically prove the 'correctness' of a computer program... 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?

32 points by gtani 14y 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.

lutze 14y 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 14y 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.
- fusiongyro 14y 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?
  - enraged_camel 14y 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.
    - deleted 14y ago
      [deleted]
    - calhoun137 14y ago
      Just because something is a consensus doesn't make it true. And its not a consensus, its just the majority view that a minority of us find incredibly backwards. Just because you can get away with something doesn't mean its a good idea either. You can get away with a lot in programming, back yourself into a corner, and hack your way out, does that mean since you can get away with it that its a good idea to program like that?
  - lutze 14y 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!
    - fusiongyro 14y ago
      The problem is that these tools don't help much. In other fields, people clamor for software because software can excel at things humans are bad at: repetitive tasks, rote calculations, lots of arithmetic. The hard part of the proof is coming up with it, not checking it. And coming up with the proof requires deep insights, which means a library of proofs isn't as useful as a library of code where you can use the code without having to understand it. What we have so far is pretty good at checking proofs but very bad at coming up with them. So what you're actually engaging in here is "machine-centric bigotry"--the idea that the machine is intrinsically better at all problem solving than man, despite evidence to the contrary. 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.
- eric-hu 14y 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.
strangestchild 14y 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.
- Someone 14y ago
  Nontrivial, but doable. See #11 in http://www.cs.ru.nl/~freek/100/ http://www.cs.ru.nl/~freek/100/ Also: http://us.metamath.org/mpegif/infpn.html http://us.metamath.org/mpegif/infpn.html
  - fusiongyro 14y ago
    I think it supports strangestchild's thesis that all five proofs from this page[1] would fit on a page and a half printed but the Coq proof (the only one I could find a download for from your list) is 825 lines of code. [1]: http://primes.utm.edu/notes/proofs/infinite/ http://primes.utm.edu/notes/proofs/infinite/
    - Someone 14y ago
      You can easily fit all of them on one page, as long as you build enough scaffolding theorems to get there. I am not that familiar with the field, but http://us.metamath.org/mpegif/infpnlem2.html 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 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 http://us.metamath.org/mpegif/a1i.html "if A is true, then anything implies it" and http://us.metamath.org/mpegif/ax-mp.html http://us.metamath.org/mpegif/ax-mp.html "if A is true and A implies B, then B is true"
walrus 14y 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.
gtani 14y ago
Yeah, pretty fluffy article, no mention of HOL, dependent types, other camps. I was hoping to see libs like Isabelle, metaMath, Corbineau's coq lib etc mentioned
- szany 14y ago
  There was a mention of dependent types.
- dubya 14y ago
  Isabelle was used for the proof of the prime number theorem. The link from the article: http://repository.cmu.edu/cgi/viewcontent.cgi?article=1032&context=philosophy http://repository.cmu.edu/cgi/viewcontent.cgi?article=1032&#...
xamuel 14y 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.
- marchdown 14y ago
  I'm not sure that it's appropriate to ask, but I would love to see the paper.
  - xamuel 14y ago
    Here is the paper: http://arxiv.org/abs/1105.4135 http://arxiv.org/abs/1105.4135 And here is the formalization of sections 2-3 in Coq: http://www.math.osu.edu/~alexander.421/mech.txt http://www.math.osu.edu/~alexander.421/mech.txt
    - marchdown 14y ago
      Thanks.

gems 14y ago

How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers? You can't ask the computer to enumerate the solutions for you. You have to reason in a roundabout way, possibly building some abstraction. 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.

meaty 14y ago
That is until a computer is capable of reason, which I personally think will never happen. I'm not suggesting some other technology will not be able to reason, but it's not going to be a jumped up Turing machine.
xyzzy123 14y ago
> How does a computer help when you have conjectures involving infinite mathematical structures or extremely large numbers? Basically, you hop up a level (go meta). Instead of working with the extremely large numbers or sets, you symbolically manipulate statements about them.
- gems 14y ago
  Give me an example of how this is done or can be done.
  - sharkbot 14y ago
    Check out Adam Chlipala's Coq tutorial, specifically the section on infinite proofs: http://adam.chlipala.net/cpdt/html/Coinductive.html http://adam.chlipala.net/cpdt/html/Coinductive.html 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.

d4vlx 14y ago

No http://en.wikipedia.org/wiki/Betteridges_law_of_headlines http://en.wikipedia.org/wiki/Betteridges_law_of_headlines

walrus 14y ago

If you find this sort of thing interesting, you may enjoy A=B by Marko Petkovsek, Herbert Wilf, and Doron Zeilberger. (Wilf was mentioned in the article.) It's available for download at http://www.math.upenn.edu/~wilf/AeqB.html http://www.math.upenn.edu/~wilf/AeqB.html

jonahkagan 14y ago
Link seems to be down, but I'd be interested.
- walrus 14y ago
  If you're still having trouble accessing it, here are direct links to the mirrors: http://www.math.upenn.edu/~wilf/AeqB.pdf http://www.math.upenn.edu/~wilf/AeqB.pdf http://www.math.rutgers.edu/~zeilberg/AeqB.pdf http://www.math.rutgers.edu/~zeilberg/AeqB.pdf http://www.fmf.uni-lj.si/aeqb/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.
dubya 14y ago
I would like to add that Doron Zeilberger's opinions page is very interesting: http://www.math.rutgers.edu/~zeilberg/OPINIONS.html http://www.math.rutgers.edu/~zeilberg/OPINIONS.html

fractallyte 14y ago

One of the reciprocal outcomes of this could be method(s) to mathematically prove the 'correctness' of a computer program... 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?