[math-fun] psycho-history, etc
Hello, there are 2 recent news that are worth looking at : http://singularityhub.com/2011/08/29/pre-cog-is-real-%E2%80%93-new-software-... http://singularityhub.com/2011/09/25/supercomputer-predicts-revolution/ This reminds me of that old idea of Isaac Asimov about psycho-history that everybody found kind of way out at the time (including me)!, This means that with enough computer juice and a suitable set of data, like hundreds of millions of articles an heuristic program can predict 'something'. A good question is, they had this Watson machine capable of answering a general question, then this engine that can predict a political movement and that later one that can predict human behaviour, then what's next ?? Best regards, Simon Plouffe
Predicting what the machine will predict....(recurse) On 26 Sep 2011, at 00:15, Simon Plouffe wrote:
Hello,
there are 2 recent news that are worth looking at :
http://singularityhub.com/2011/08/29/pre-cog-is-real-%E2%80%93-new-software-...
http://singularityhub.com/2011/09/25/supercomputer-predicts-revolution/
This reminds me of that old idea of Isaac Asimov about psycho-history that everybody found kind of way out at the time (including me)!,
This means that with enough computer juice and a suitable set of data, like hundreds of millions of articles an heuristic program can predict 'something'.
A good question is, they had this Watson machine capable of answering a general question, then this engine that can predict a political movement and that later one that can predict human behaviour, then what's next ??
Best regards, Simon Plouffe
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
People are already trying to game the financial markets by watching Twitter feeds. I wouldn't be surprised if this kind of info isn't being used to predict and/or affect elections. I read the article about predicting revolutions, but they didn't say when to expect a revolution here in the U.S. At 04:15 PM 9/25/2011, Simon Plouffe wrote:
Hello,
there are 2 recent news that are worth looking at :
http://singularityhub.com/2011/08/29/pre-cog-is-real-%E2%80%93-new-software-...
http://singularityhub.com/2011/09/25/supercomputer-predicts-revolution/
This reminds me of that old idea of Isaac Asimov about psycho-history that everybody found kind of way out at the time (including me)!,
This means that with enough computer juice and a suitable set of data, like hundreds of millions of articles an heuristic program can predict 'something'.
A good question is, they had this Watson machine capable of answering a general question, then this engine that can predict a political movement and that later one that can predict human behaviour, then what's next ??
Best regards, Simon Plouffe
Yes, but I can bet they would not tell anybody if something heavy would come within usa. ? but more constructively, I am wondering what kind of intelligent answer a machine will be capable of telling to us when we will successfully be able to do OCR on math books at large. There are millions of them + all the articles on Arxiv and such places. Already there is a base of knowledge being constructed based on all the data within wikipedia in all languages called YAGO, it can be downloaded for the ones that like to experiment on these matters. Also there is a base available from google, it is the raw result of all the scanning they have been doing on books, it is available to anybody, I searched into it, interesting but it contains (in french for example) a lot of garbage data. Can a machine do mathematics and inference if it has millions of mathematical identities translatable into maple or mathematica ??? a kind of omega machine (after wolfram alpha, n'th version)... simon plouffe Le 26/sept./2011 06:30, Henry Baker a écrit :
People are already trying to game the financial markets by watching Twitter feeds.
I wouldn't be surprised if this kind of info isn't being used to predict and/or affect elections.
I read the article about predicting revolutions, but they didn't say when to expect a revolution here in the U.S.
At 04:15 PM 9/25/2011, Simon Plouffe wrote:
Hello,
there are 2 recent news that are worth looking at :
http://singularityhub.com/2011/08/29/pre-cog-is-real-%E2%80%93-new-software-...
http://singularityhub.com/2011/09/25/supercomputer-predicts-revolution/
This reminds me of that old idea of Isaac Asimov about psycho-history that everybody found kind of way out at the time (including me)!,
This means that with enough computer juice and a suitable set of data, like hundreds of millions of articles an heuristic program can predict 'something'.
A good question is, they had this Watson machine capable of answering a general question, then this engine that can predict a political movement and that later one that can predict human behaviour, then what's next ??
Best regards, Simon Plouffe
This may be a good time to put in another plug for something I've wished for for years. I want every mathematical fact on Wikipedia to come complete with one or more proofs linked to it. Furthermore, as theorem-proving technology advances, I would like each proof to be machine-checkable. Is there any way to notify Wikipedia that a statement is a mathematical fact, so that Wikipedia will ask you to link to a proof? Mathematics -- unlike any other field -- has a built-in capability for eliminating B.S. In mathematics we don't survey the experts to determine if something is true; we _prove_ it true. Proof in hand, we no longer need the experts. In mathematics, a long & successful career won't insulate you from people checking your proofs -- on the contrary, your proofs are even more likely to be swiftly challenged. At 10:13 PM 9/25/2011, Simon Plouffe wrote:
Can a machine do mathematics and inference if it has millions of mathematical identities translatable into maple or mathematica ??? a kind of omega machine (after wolfram alpha, n'th version)...
This may be a good time to put in another plug for something I've wished for for years.
I want every mathematical fact on Wikipedia to come complete with one or more proofs linked to it. Furthermore, as theorem-proving technology advances, I would like each proof to be machine-checkable.
Machines cannot check general mathematical proofs, due to Gödel's Incompleteness Theorem. Indeed, if they could, mathematicians would quickly be rendered obsolete, as a computer could soon perform a breadth-first search of proofs. Sincerely, Adam P. Goucher
From: Adam P. Goucher <apgoucher@gmx.com> To: math-fun <math-fun@mailman.xmission.com> Sent: Friday, September 30, 2011 7:36 AM Subject: Re: [math-fun] psycho-history, etc
This may be a good time to put in another plug for something I've wished for for years.
I want every mathematical fact on Wikipedia to come complete with one or more proofs linked to it. Furthermore, as theorem-proving technology advances, I would like each proof to be machine-checkable.
Machines cannot check general mathematical proofs, due to Gödel's Incompleteness Theorem. Indeed, if they could, mathematicians would quickly be rendered obsolete, as a computer could soon perform a breadth-first search of proofs.
Sincerely,
Adam P. Goucher
_______________________________________________
Humans can check mathematical proofs, so machines should also be able to. Gödel'sIncompleteness Theorem asserts that there are propositions that cannot be proved within a given axiom system, but which are true in an interpretation that steps outside that axiom system. It is perfectly possible for a computer to generate a list in which any proof will eventually appear. Mathematicians are useful because they selectively prove theorems that are interesting to their readers. -- Gene
Not true. All legitimate proofs are machine-checkable, but coming up with such a proof is a non-computable exercise. Now a machine-checkable proof may be a bit more tedious to read, just as reading machine code is more tedious than reading C/Lisp/Java/whatever, because every bit of detail must be written out. However, once such a project gets off the ground, the large number of little lemmas required will eventually be already incorporated into such a Wikipedia, enabling reasonably short machine-checkable proofs to be expressed. At 07:36 AM 9/30/2011, Adam P. Goucher wrote: Machines cannot check general mathematical proofs, due to Gödel's
Incompleteness Theorem. Indeed, if they could, mathematicians would quickly be rendered obsolete, as a computer could soon perform a breadth-first search of proofs.
On that note, Metamath (http://us.metamath.org) has actually gone ahead and done a lot of this work. It fully develops group, field, ring, and vector space theory from ZFC, and also has a complete construction of the real and complex numbers included. It's very cool: you should check it out. -Scott On Fri, Sep 30, 2011 at 10:50 AM, Henry Baker <hbaker1@pipeline.com> wrote:
Not true. All legitimate proofs are machine-checkable, but coming up with such a proof is a non-computable exercise.
Now a machine-checkable proof may be a bit more tedious to read, just as reading machine code is more tedious than reading C/Lisp/Java/whatever, because every bit of detail must be written out. However, once such a project gets off the ground, the large number of little lemmas required will eventually be already incorporated into such a Wikipedia, enabling reasonably short machine-checkable proofs to be expressed.
At 07:36 AM 9/30/2011, Adam P. Goucher wrote: Machines cannot check general mathematical proofs, due to Gödel's
Incompleteness Theorem. Indeed, if they could, mathematicians would quickly be rendered obsolete, as a computer could soon perform a breadth-first search of proofs.
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
Well, proofs are recursively enumerable, so if there is a proof, a machine can (eventually, but not necessarily practically) find it. And if you restrict your proofs to some maximum length, then it is computable whether or not a "not-too-long" proof exists. I think the real problem is proving that what you ask a machine to prove is a correct translation of what you actually meant. This is a similar problem to proving programs correct--the description of what it means to be correct may not match what the program is really supposed to do. --ms On 9/30/2011 10:50 AM, Henry Baker wrote:
Not true. All legitimate proofs are machine-checkable, but coming up with such a proof is a non-computable exercise.
Now a machine-checkable proof may be a bit more tedious to read, just as reading machine code is more tedious than reading C/Lisp/Java/whatever, because every bit of detail must be written out. However, once such a project gets off the ground, the large number of little lemmas required will eventually be already incorporated into such a Wikipedia, enabling reasonably short machine-checkable proofs to be expressed.
At 07:36 AM 9/30/2011, Adam P. Goucher wrote: Machines cannot check general mathematical proofs, due to Gödel's
Incompleteness Theorem. Indeed, if they could, mathematicians would quickly be rendered obsolete, as a computer could soon perform a breadth-first search of proofs.
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
participants (7)
-
Adam P. Goucher -
David Makin -
Eugene Salamin -
Henry Baker -
Mike Speciner -
Scott Fenton -
Simon Plouffe