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.
Talk about revolutionary, true automated pure math would be a human milestone on par with very few developments in history.
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?
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.
Hilbert thought so too, but it is proveably not to be (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), 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.)
Given that human beings do mathematics just fine, I think there might be some way to deal with this.
I'll put up a blog post soon on this!
http://monasandnomos.org/2012/12/05/the-idea-of-a-characteri...
http://vanemden.wordpress.com/2012/04/08/flowcharts-the-once...
