Computational Knowledge and the Future of Pure Mathematics (opens in new tab)

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!

Nonetheless, I point out that I did not claim that human input was essential either for finding or proving interesting theorems (although proveable results about (non-)computeability seem as close as one could get to such a statement!), but only that math could never be completely automated (or, to use what, as you implicitly point out, is a more appropriate term, even formalised).

I'm confused by this response.

Certainly I am not claiming that no mathematics can be done, but equally certainly there is a lot of math that seems, at least "at our present level of (mental) technology", to be out of human reach. Since it is (I think) precisely this sort of math in which Wolfram is most interested, it seems odd to point out the math that humans can do as a counterexample.

(I am further confused because it seems to me that the sets of tasks that humans can perform easily and that computers can perform easily are, if not disjoint, at least of very small overlap, so that it might not be unreasonable to take the presence of a task in one set as reason to question its membership in the other.)

"So in principle one can imagine having a system that takes input and generates “interesting” theorems about it."

I can imagine having a spaceship that goes faster than light, too. It is more than slightly harder to actually build it.

Generating theorems is easy (it may even be possible to generate all theorems in order of increasing length of their proof and not get stuck into generating evermore longer proofs of theorems encountered earlier, but I am not sure of that)

However, we have only very faint ideas about what constitutes an interesting theorem (are theorems even dull or interesting independent of their known proofs? if one finds a new interesting proof for a theorem that previously only had a dull proof, I think the theorem can become less dull), and certainly do not know how to programmatically discriminate them from dull ones.

> 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) 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 .