Are Mathematicians In Jeopardy?
rjlipton.wordpress.com
rjlipton.wordpress.com
So my take is that he's not necessarily wrong, but if he's right then lack of employment for mathematicians won't be our biggest concern.
This is wrong. There are lots of branches of computer science that are not math, nor dependent on new math.
Imagine a future where, in addition to checking your spelling and grammar, your computer could check your logic too!
For example, in Einstein's Special Theory, there's not a lot of deep mathematics (relative to the General Theory) so it's not too difficult to imagine Watson taking the problem and axiomatizing (just to see what would happen) that light speed is always constant (which is the key to everything else that followed).
But what about Descarte's insight that geometry could be described by algebra using a coordinate system, giving birth to analytic geometry? Or proving that it can't prove all true statements in arithmetic (Godel)? Or even asking the question?
I think we're a long way off from doing something like that in a machine.
On the other hand, journal papers keep pouring every day at rates that are impossible to keep up. In the future this situation will be hopeless in the absence of some AI to guide us among that mess. But then again, papers are written in a combination of natural language and mathematics.
This was a new model which made a large class of insights more tractable to human minds. A theorem-finding computer probably wouldn't come up with the same kind of model(unless we specifically programmed it to), it would come up with models which made further insights more tractable to theorem-finding computers. Already, today, a huge part of the problem with creative computers is interpreting their results for humans.
However, other automated proofs have not been so lucky: Hale's proof of the Kepler Conjecture was 300 pages of mathematics and 40,000 lines of supporting computer code, and the referees of the paper tried four years to understand it (they even set up a seminar series for all of the prerequisite material to understand the proof) before letting the authors know that they were unable to verify the correctness of the proof because they "ran out of energy to devote to the problem." (The Annals of Mathematics henceforth edited their rules to disallow submission of computer programs.) The Flyspeck project is to, well, ask a program to verify the correctness of the proof. Ah, the times we live in.
So, he not only wants correct formal proofs of difficult theorems, but also insights and thoughtful conjectures? I think math is a red herring here, what he really wants is strong AI -- you can put 'writers' or 'economists' in his arguments and not much changes.
Watson won't be able to assign a truth value to this gramatically correct sentence, but would it have the insight that it just stumbled upon a philosophical problem that's solved by narrowing the notion of truth it uses (Bertrand Russell).
In other words, a machine may not be able to examine itself in the way that humans can when certain problems arise.
Also, the limits of computation have been given an upper bound. If it's not computable by a Turing machine with a finite memory tape (or anything else that is mappable to a Turing machine with a finite memory tape), it's not computable by a physical computer.
Steve Yegge started exploring the metaphysics of computer programs before he stopped blogging; it makes for interesting reading.
(As far as I know, neurons can be approximated well enough by classical computers and you don't even need to go quantum, but that's another story.)
Am not going to argue whether a machine can "really" be alive, "really" be self-aware. Is a virus self-aware? Nyet! How about oyster? I doubt it. A cat? Almost certainly. A human? Don't know about you tovarishch, but I am. Somewhere along evolutionary chain from macromolecule to human brain self-awareness crept in. Psychologists assert it happens automatically whenever a brain acquires certain very high number of associational paths. Can't see it matters whether paths are protein or platinum.
By a physical Turing equivalent computer. True. The breakthrough will come when we'll be able to overcome the damnation of step-by-step-ness (which is the primitive expression of causality).
It already happens for 1/0 answers.
If you compare it to chess then the computer programs are still at the beginner level. First year math students will be able to prove things that the computer cannot, yet.
It's an intriguing area. Computer programs can perfectly well check whether a proof is correct, so in principle all you have to do is enumerate all "proofs" and pick out the valid ones. In practice the research is focused on doing this search more efficiently and intelligently.
Watson may represent the ultimate "second opinion."
I absolutely believe that Watson could revolutionize health care, but not in the way most people are suggesting. Despite what you see on House MD, diagnosing mystery illnesses is not something that doctors struggle with.
However, the amount of money that Watson could recover in insurance and medicare fraud would absolutely dwarf what he won on Jeopardy. There's the real payoff...
But there's no need for watson. there's already good enough expert systems for this job. for example see isabel healthcare.
The issues in automating medicine are more business and cultural and much less technological.
Many years ago I was on a logic conference and one speaker proposed to make "a computer can solve it automatically" the definition of trivial (as in "this is trivial to solve").
Specifically, a computer spitting out proofs of things that no one asked for doesn't seem especially productive. Humans conjecturing something interesting and getting computer generated proofs or counter-examples seems interesting and more plausible though.
Anyone that's tried to use a state-of-the-art automated theorem prover (like ACL2) knows we have a long, long way to go.
They're still pretty dumb.
That said, I'm convinced that Godels Incompleteness Theorems hold only in the limit -- the majority of propositions of human interest are probably amenable to mechanical proving.
I wouldn't have guessed even 3 years ago that we were this close to having a working Jeopardy player.
http://www.math.upenn.edu/~wilf/AeqB.html
The authors reduce the proving of a wide class of combinatorial identities, which were formerly regarded as extremely nontrivial, to a mechanical calculation. This has been implemented in Maple. Input your favorite identity, push the button, and watch the computer spit out a proof.
This answers the question, I believe. Are all human mathematicians in jeopardy? No.
May we need less human mathematicians in the future and maintain a strong mathematical community? Likely.
Still, in 15 years? I'll wager against this prediction.
It means hold on to your hat Dorthy, cause Kansas is going byebye.
Hilbert tried to come up with a method of generating theorems by just cranking a wheel that churns out different logical forms. Ends up that we still need verification to make sure that these things actually make _sense_. (Even if we have incompleteness in any logical system that contains arithmetic, we still have to figure out whether a certain logical form "makes sense" to use.)
The incompleteness theorems are a barrier to creating a "perfect" mathematician, but certainly not a barrier to creating an adequate one.
Or are you trying to say that a computer would have no idea which theorems were interesting and which were dull?
The fact that there are results the computer can't prove is not a bar to it being useful. After all there are results we can't prove either.
What was discussed was not a perfect theorem proving system. But rather a system that was good enough to be competitive with humans.
1. The incompleteness theorems basically say, "if you have a logical system that includes Peano arithmetic, even if the theory is consistent, it will be an incomplete system." Also, "if you're trying to show that said system is consistent within the system, then you have an inconsistent system." These statements drop the Hilbert program to a dead halt.
2. I'm not talking about a perfect theorem proving system. However, what I _am_ saying is that you still need humans to verify the results - we do have automatic theorem provers already, but we still need to make sure that the steps are logical. Not only that, but the theorem needs to connote something useful. Also, we tend to use axioms that we can't say are consistent within the system (for instance, the axiom of choice; yet, mathematicians use it like candy in order to show useful results in analysis, and weird, unintuitive results in topology [slicing a sphere and producing two spheres with the same volume.]) I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack.
3. The reason why I'm doubtful that we'd ever see such an AI for proving math statements is because the entire enterprise is still very much a creative one - you not only have to generate the logical forms somehow, but also figure out whether it gets you closer to your goal or not. I suppose you could have some sort of heuristic that could show that a generated theorem or lemma could in fact get you closer to your goal, but my god, math is filled with so many potholes and garden paths that could lead one astray.
Don't get me wrong, it'd be awesome to see such a system - however, I'm very doubtful that such a system could ever be created, and if it is created, that it'd be actually useful to practicing mathematicians.
Let's see.
The incompleteness theorems basically say, "if you have a logical system that includes Peano arithmetic, even if the theory is consistent, it will be an incomplete system." Also, "if you're trying to show that said system is consistent within the system, then you have an inconsistent system." These statements drop the Hilbert program to a dead halt.
Close but not quite. The incompleteness theorem says that a consistent set of axioms describes arithmetic can only be consistent if and only if it does not prove its own consistency. An inconsistent theorem proves absolutely everything. A consistent system is welcome to attempt to prove its own consistency all it likes - it will just fail.
It is true that this killed Hilbert's program as originally conceived.
I'm not talking about a perfect theorem proving system. However, what I _am_ saying is that you still need humans to verify the results - we do have automatic theorem provers already, but we still need to make sure that the steps are logical.
At some point, I fail to see why you need the humans. What value are humans actually providing?
Not only that, but the theorem needs to connote something useful.
Mathematicians already have a concept of "useful" that is so far at odds with the common understanding of the term that I honestly cannot make sense of what "useful" actually means in this context. If the program is able to tackle actual difficult research problems, and has heuristics that suffice for real problems, then its notion of "useful" is probably good enough for practice.
Also, we tend to use axioms that we can't say are consistent within the system (for instance, the axiom of choice; yet, mathematicians use it like candy in order to show useful results in analysis, and weird, unintuitive results in topology [slicing a sphere and producing two spheres with the same volume.])
Outside of logic, most of mathematics has agreed on the set of axioms to use. Namely ZFC. As for using axioms that are not consistent within the system, that is absolutely necessary by the incompleteness theorem. Though you picked an ironically bad example. Gödel proved that ZF is consistent if and only if ZFC is consistent, and therefore the axiom of choice does not affect the consistency of the axiom system. It might not describe the set theory we want to describe, but it does not lead to contradictions.
I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack.
That was one of the weaker points made. I see the value of having heuristics that can go astray. But if you've got this in a computer, hook the heuristics up to a theorem prover that can fill in the details and come up with verified theorems. And which can alternately can describe useful plans of attacks.
I understand that the article is saying, "yes, such a proof produced by a computer still needs to be independently verified." To be honest, I think a system that could make mistakes and whatnot is not necessarily what people would want to see - reason being that mathematicians probably have not much trouble trying to figure out the larger details and overall plan of attack.
Until people trust the computer, it absolutely needs to be double-checked. Any piece of software can have horrible bugs that are hard to find. No matter how confident its designers are, it needs verification.
The reason why I'm doubtful that we'd ever see such an AI for proving math statements is because the entire enterprise is still very much a creative one - you not only have to generate the logical forms somehow, but also figure out whether it gets you closer to your goal or not. I suppose you could have some sort of heuristic that could show that a generated theorem or lemma could in fact get you closer to your goal, but my god, math is filled with so many potholes and garden paths that could lead one astray.
Yes, it looks as far away from being possible now as beating Jeopardy looked back when Deep Blue beat Kasparov. Based on my experience with mathematics and computing I find myself in agreement with rjlipton that it is not impossible, and in fact I wouldn't be surprised to see it happen within 15 years.
Here is an interesting back of the envelope calculation for you. A human brain has 100 billion neurons, each of which has 7000 connections, and fires about every tenth of a second. Let's suppose that emulation averages 1000 clock cycles per synapse. The result is that simulating something as complex as the human brain in real time should take on the order of 1011 * 7000 * 1000 = 71017 clock cycles per second. Watson was running at 81012 clock cycles per second. If Moore's Law continues to hold for 16 generations, which is 24 years, then a computer the size of Watson should be able to match the human brain, in real time.
Once we have the hardware, I think it is only a question of time until the necessary software is available. And given the demonstrated power of statistical analysis of large data sets to real problems (think Watson, Google translate, and the like), I think we're on our way to developing appropriate software as well.
Don't get me wrong, it'd be awesome to see such a system - however, I'm very doubtful that such a system could ever be created, and if it is created, that it'd be actually useful to practicing mathematicians.
I think that rjlipton is a little optimistic on the time frame. But I fully expect to see it arrive in my lifetime. I have some trepidation about the inevitable economic upheaval when it does happen.