"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.
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) 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 .
Someone|11 years ago
"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.
JadeNB|11 years ago
> 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 .
kazagistar|11 years ago