As Math Grows More Complex, Will Computers Reign?(wired.com)
wired.com
As Math Grows More Complex, Will Computers Reign?
http://www.wired.com/wiredscience/2013/03/computers-and-math/
5 comments
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.
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.
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
Also: http://us.metamath.org/mpegif/infpn.html
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/
[1]: http://primes.utm.edu/notes/proofs/infinite/
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 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"
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"
Yes, well, I suppose I could fit all of Firefox on one page as long as you only look at the main() function and not any of the functions that lead up to it. But that doesn't really tell you much about Firefox, does it? And the fact that there are primitives like pthread_create() and pow() underneath at sufficiently low level doesn't really say much either.
Yes, but like that 'main', all those short proofs are full of holes. For example, Euclid assumes readers know what he means when he talks of prime numbers, what multiplication and division are, how they work. For example, given p and q, how many different r's can there be such that r=p/q? Given n and p>1, how do we know p does not divide n * p + 1? Is it always possible to write a number as a product of primes?
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.
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.
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.
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.
> 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?
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?
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!
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!
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.
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.
The last part was a joke, calm down dear.
Edit: As for psychologists, you're seriously telling me you never heard of Licklider? That's... astounding.
http://en.wikipedia.org/wiki/J._C._R._Licklider
Edit: As for psychologists, you're seriously telling me you never heard of Licklider? That's... astounding.
http://en.wikipedia.org/wiki/J._C._R._Licklider
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.
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.
>>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.
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]
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 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.
Here is the paper: 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
Thanks.
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.
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.
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.
Check out Adam Chlipala's Coq tutorial, specifically the section on infinite proofs: 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.
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.
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.
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?
How does a computer build abstractions on its own?
How does it build them? That's not a simple question, but it's possible to do. E.g. machine learning is computers building abstractions.
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.
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.
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
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):
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.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?
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?
Also, the point of not having standard programming classes leads to a lack of standards in research coding is an important one.