4 ms·

Computational Knowledge and the Future of Pure Mathematics

126 points by kylemaxwell 12y ago

pnut 12y ago
Can some bored billionaire please throw $100M at this project? Talk about revolutionary, true automated pure math would be a human milestone on par with very few developments in history.
- igravious 12y ago
  I'm confused why you would say that. FTA: > Ultimately every named construct or concept in pure mathematics needs to have a place in our symbolic language. The reason your plea confuses me is that I don't understand the social value in encoding all _public_ "named construct or concept" in a _private_ "symbolic language" that only one proprietary piece of software that can be monetized by one corporation can benefit from? Why would we want to do that?
  - dwpdwpdwpdwpdwp 12y ago
    We would want to do that for the same reasons that people write textbooks. Mathematica was not designed for building applications like Java or C++, but as a tool for research and learning. To that end, Mathematica is well designed and the documentation is exceptionally curated, just like, for example, a physics textbook, which also encodes public knowledge in a private (copyrighted) manner. The mathematicians and software engineers at Wolfram Research should be compensated for their efforts, just like the authors and publishers of textbooks. And I'd much rather pay for my textbooks than see them filled with ads. As a lover of mathematics I'm happy to see people writing and thinking about the ideas in this post. It's a noble pursuit.
    - igravious 12y ago
      Your analogy textbook <-> mathematical software does not hold. Think it through. It's not a copyright issue. I can explain in detail my point of view if you like. It's not a noble pursuit when the gain is too one-sided. Wolfram and his company would accrue to much material advantage at the expense of an open and public mathematical discourse. This much is plain to see, watch out for rhetoric of the kind on display in that post!
- JadeNB 12y ago
  > Talk about revolutionary, true automated pure math would be a human milestone on par with very few developments in history. Hilbert thought so too, but it is proveably not to be (http://en.wikipedia.org/wiki/Entscheidungsproblem http://en.wikipedia.org/wiki/Entscheidungsproblem), no matter how much money is thrown at it by how many bored billionaires. (EDIT: To be clear, I am not claiming that there is no room for automated assistance of pure math, only that it can never be wholly automated.) (Second, important EDIT: As Khaki points out (https://news.ycombinator.com/item?id=8170062 https://news.ycombinator.com/item?id=8170062), I should make it clearer that many objections about what computers can't do apply equally well to show what humans also can't do.)
  - diakopter 12y ago
    Wolfram's essay addresses this point...
    - JadeNB 12y ago
      Life's too short to read Wolfram when he gets going, so I only skimmed it; but: where? I see: > In a sense an axiom system is a way of giving constraints too: it doesn’t say that such-and-such an operator “is Nand”; it just says that the operator must satisfy certain constraints. And even for something like standard Peano arithmetic, we know from Gödel’s Theorem that we can never ultimately resolve the constraints–we can never nail down that the thing we denote by “+” in the axioms is the particular operation of ordinary integer addition. Of course, we can still prove plenty of theorems about “+”, and those are what we choose from for our report. and: > But there will inevitably be some limitations—resulting in fact from features of mathematics itself. For example, it won’t necessarily be easy to tell what theorem might apply to what, or even what theorems might be equivalent. Ultimately these are classic theoretically undecidable problems—and I suspect that they will often actually be difficult in practical cases too. And at the very least, all of them involve the same kind of basic process as automated theorem proving. Are these what you mean? Both of these seem to amount to, "Sure, mathematicians say you can't do it, but I hold out hope", an argument which is no more persuasive than one would expect to find from various circle-squarers. Less subjectively, they both seem to miss the point; the incompleteness results, for example, do not just say that certain theorems aren't clearly specified, or are equivalent to unknown other theorems, or vague things like that, but specifically that there are true but unproveable theorems—putting paid to any attempt at complete automation. I emphasise again that this is only a knock if you dream grandiosely of capturing all of mathematics in an automated (or, as Khaki pointed out above (https://news.ycombinator.com/item?id=8170062 https://news.ycombinator.com/item?id=8170062) that I should really be saying, even formal but human-constructed) framework; it says nothing about the feasibility of automated theorem-proving for some results, and, indeed, we have a success story for one such result on the front page even now: https://news.ycombinator.com/item?id=8169686 https://news.ycombinator.com/item?id=8169686 .
- kazagistar 12y ago
  I would rather they build one that does not lock people in to a single proprietary product run by an egomaniac.
diakopter 12y ago
some related and well-reasoned, well-written essays: http://monasandnomos.org/2012/12/05/the-idea-of-a-characteristica-universalis-between-leibniz-and-russell-and-its-relevancy-today/ http://monasandnomos.org/2012/12/05/the-idea-of-a-characteri... http://vanemden.wordpress.com/2012/04/08/flowcharts-the-once-and-future-programming-language/ http://vanemden.wordpress.com/2012/04/08/flowcharts-the-once...
kevinwang 12y ago
Absolutely fascinating. Stoked to see where this'll go!
fiatmoney 12y ago
This is very similar to Doug Lenat's work on Automated Mathematician & later on Eurisko, and later Ken Haase's follow up work on representation languages. http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=html&identifier=ADA155378 http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=ht... There were severe sticking points around the cultivation of an idea of "interesting" properties and the performance issues around evaluating a combinatoric space of possible manipulations. There hasn't been serious work along those lines since the early 90s or so. It's annoying because especially Haase's work has some very practical insights, but Wolfram seems to be loathe to ever admit he's building off of someone else's work.
- mjn 12y ago
  Yes! I wish there was more work in that line. Very interesting work, but also hit some major problems. This 1984 postmortem paper by Lenat and a collaborator is also thought-provoking: http://eksl.isi.edu/files/library/Lenat_Brown-1984-why-AM-and-EURISKO-work.pdf http://eksl.isi.edu/files/library/Lenat_Brown-1984-why-AM-an...
bkirwi 12y ago
I find it odd that Wolfram talks about all the thousands of things that will need to be 'built in' to Mathematica for this project to work -- shouldn't you be able to implement these things in the language itself?
jaan 12y ago
Very cool - I'm working on a related project: https://www.google-melange.com/gsoc/project/details/google/gsoc2014/jaanaltosaar/5741031244955648 https://www.google-melange.com/gsoc/project/details/google/g... I'll put up a blog post soon on this!

126 points by kylemaxwell 12y ago

pnut 12y ago

Can some bored billionaire please throw $100M at this project? Talk about revolutionary, true automated pure math would be a human milestone on par with very few developments in history.

igravious 12y ago
I'm confused why you would say that. FTA: > Ultimately every named construct or concept in pure mathematics needs to have a place in our symbolic language. The reason your plea confuses me is that I don't understand the social value in encoding all _public_ "named construct or concept" in a _private_ "symbolic language" that only one proprietary piece of software that can be monetized by one corporation can benefit from? Why would we want to do that?
- dwpdwpdwpdwpdwp 12y ago
  We would want to do that for the same reasons that people write textbooks. Mathematica was not designed for building applications like Java or C++, but as a tool for research and learning. To that end, Mathematica is well designed and the documentation is exceptionally curated, just like, for example, a physics textbook, which also encodes public knowledge in a private (copyrighted) manner. The mathematicians and software engineers at Wolfram Research should be compensated for their efforts, just like the authors and publishers of textbooks. And I'd much rather pay for my textbooks than see them filled with ads. As a lover of mathematics I'm happy to see people writing and thinking about the ideas in this post. It's a noble pursuit.
  - igravious 12y ago
    Your analogy textbook <-> mathematical software does not hold. Think it through. It's not a copyright issue. I can explain in detail my point of view if you like. It's not a noble pursuit when the gain is too one-sided. Wolfram and his company would accrue to much material advantage at the expense of an open and public mathematical discourse. This much is plain to see, watch out for rhetoric of the kind on display in that post!
JadeNB 12y ago
> Talk about revolutionary, true automated pure math would be a human milestone on par with very few developments in history. Hilbert thought so too, but it is proveably not to be (http://en.wikipedia.org/wiki/Entscheidungsproblem http://en.wikipedia.org/wiki/Entscheidungsproblem), no matter how much money is thrown at it by how many bored billionaires. (EDIT: To be clear, I am not claiming that there is no room for automated assistance of pure math, only that it can never be wholly automated.) (Second, important EDIT: As Khaki points out (https://news.ycombinator.com/item?id=8170062 https://news.ycombinator.com/item?id=8170062), I should make it clearer that many objections about what computers can't do apply equally well to show what humans also can't do.)
- diakopter 12y ago
  Wolfram's essay addresses this point...
  - JadeNB 12y ago
    Life's too short to read Wolfram when he gets going, so I only skimmed it; but: where? I see: > In a sense an axiom system is a way of giving constraints too: it doesn’t say that such-and-such an operator “is Nand”; it just says that the operator must satisfy certain constraints. And even for something like standard Peano arithmetic, we know from Gödel’s Theorem that we can never ultimately resolve the constraints–we can never nail down that the thing we denote by “+” in the axioms is the particular operation of ordinary integer addition. Of course, we can still prove plenty of theorems about “+”, and those are what we choose from for our report. and: > But there will inevitably be some limitations—resulting in fact from features of mathematics itself. For example, it won’t necessarily be easy to tell what theorem might apply to what, or even what theorems might be equivalent. Ultimately these are classic theoretically undecidable problems—and I suspect that they will often actually be difficult in practical cases too. And at the very least, all of them involve the same kind of basic process as automated theorem proving. Are these what you mean? Both of these seem to amount to, "Sure, mathematicians say you can't do it, but I hold out hope", an argument which is no more persuasive than one would expect to find from various circle-squarers. Less subjectively, they both seem to miss the point; the incompleteness results, for example, do not just say that certain theorems aren't clearly specified, or are equivalent to unknown other theorems, or vague things like that, but specifically that there are true but unproveable theorems—putting paid to any attempt at complete automation. I emphasise again that this is only a knock if you dream grandiosely of capturing all of mathematics in an automated (or, as Khaki pointed out above (https://news.ycombinator.com/item?id=8170062 https://news.ycombinator.com/item?id=8170062) that I should really be saying, even formal but human-constructed) framework; it says nothing about the feasibility of automated theorem-proving for some results, and, indeed, we have a success story for one such result on the front page even now: https://news.ycombinator.com/item?id=8169686 https://news.ycombinator.com/item?id=8169686 .
kazagistar 12y ago
I would rather they build one that does not lock people in to a single proprietary product run by an egomaniac.

diakopter 12y ago

some related and well-reasoned, well-written essays: http://monasandnomos.org/2012/12/05/the-idea-of-a-characteristica-universalis-between-leibniz-and-russell-and-its-relevancy-today/ http://monasandnomos.org/2012/12/05/the-idea-of-a-characteri... http://vanemden.wordpress.com/2012/04/08/flowcharts-the-once-and-future-programming-language/ http://vanemden.wordpress.com/2012/04/08/flowcharts-the-once...

kevinwang 12y ago

Absolutely fascinating. Stoked to see where this'll go!

fiatmoney 12y ago

This is very similar to Doug Lenat's work on Automated Mathematician & later on Eurisko, and later Ken Haase's follow up work on representation languages. http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=html&identifier=ADA155378 http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=ht... There were severe sticking points around the cultivation of an idea of "interesting" properties and the performance issues around evaluating a combinatoric space of possible manipulations. There hasn't been serious work along those lines since the early 90s or so. It's annoying because especially Haase's work has some very practical insights, but Wolfram seems to be loathe to ever admit he's building off of someone else's work.

mjn 12y ago
Yes! I wish there was more work in that line. Very interesting work, but also hit some major problems. This 1984 postmortem paper by Lenat and a collaborator is also thought-provoking: http://eksl.isi.edu/files/library/Lenat_Brown-1984-why-AM-and-EURISKO-work.pdf http://eksl.isi.edu/files/library/Lenat_Brown-1984-why-AM-an...

bkirwi 12y ago

I find it odd that Wolfram talks about all the thousands of things that will need to be 'built in' to Mathematica for this project to work -- shouldn't you be able to implement these things in the language itself?

jaan 12y ago

Very cool - I'm working on a related project: https://www.google-melange.com/gsoc/project/details/google/gsoc2014/jaanaltosaar/5741031244955648 https://www.google-melange.com/gsoc/project/details/google/g... I'll put up a blog post soon on this!