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.
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.
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.
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.
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.
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.
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?
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.
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
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.
> 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.
Essentially the same way we reason about infinite mathematical structures in our heads: we define infinite structures by a finite system of generators and prove things by induction. The computer verifies that your inductive proof is correct.
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.
The only thing I asserted in that comment was that you can't ask the computer to help you (effectively) in a naive search when the space is large or infinite. I'm not familiar with how theorem provers work, so I'm most likely wrong anyway.
How does a computer build abstractions on its own?
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.)
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.
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?
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.
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.
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.
Nontrivial, but doable. See #11 in http://www.cs.ru.nl/~freek/100/
Also: http://us.metamath.org/mpegif/infpn.html
4 replies →
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.
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.
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.
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?
7 replies →
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.
I'm not sure that it's appropriate to ask, but I would love to see the paper.
2 replies →
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
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&#...
There was a mention of dependent types.
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.
> 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.
Give me an example of how this is done or can be done.
1 reply →
Essentially the same way we reason about infinite mathematical structures in our heads: we define infinite structures by a finite system of generators and prove things by induction. The computer verifies that your inductive proof is correct.
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.
> You have to reason in a roundabout way, possibly building some abstraction.
You're assuming that computers can't handle abstractions.
The only thing I asserted in that comment was that you can't ask the computer to help you (effectively) in a naive search when the space is large or infinite. I'm not familiar with how theorem provers work, so I'm most likely wrong anyway.
How does a computer build abstractions on its own?
1 reply →
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
I would like to add that Doron Zeilberger's opinions page is very interesting: http://www.math.rutgers.edu/~zeilberg/OPINIONS.html
Link seems to be down, but I'd be interested.
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.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):
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?
No
http://en.wikipedia.org/wiki/Betteridges_law_of_headlines