Math Proving: Are Computer Derived Theorems Accurate?

[jobyts]

If we feed all the existing mathematical axioms to a powerful computer, it should be able to give us all the proofs and theorems that can be derived using the axioms. Is there anything wrong with this logic?

 

[waht]

If we feed all the existing mathematical axioms to a powerful computer, it should be able to give us all the proofs and theorems that can be derived using the axioms. Is there anything wrong with this logic?

Godel's incompleteness theorem implies that one can't go on like that. You will eventually get to theorems that are impossible to prove within the system.

http://en.wikipedia.org/wiki/Gödel's_incompleteness_theorems

 

[Mu naught]

Godel's incompleteness theorem implies that one can't go on like that. You will eventually get to theorems that are impossible to prove within the system.

http://en.wikipedia.org/wiki/Gödel's_incompleteness_theorems

He said all the provable theorems, so what you just posted is pretty irrelevant.

I think it's a good question. If proof is just manipulating a set of axioms using a certain amount of rules like in TNT I see no reason a computer couldn't generate many thousands of proofs, but they would probably be random and the vast majority be obvious or already proven.

 

[rasmhop]

If we feed all the existing mathematical axioms to a powerful computer, it should be able to give us all the proofs and theorems that can be derived using the axioms. Is there anything wrong with this logic?

Yes. At any given point in time it will only have given us finitely many theorems, but there are infinitely many (assuming a moderately interesting axiom system and a computer with finite computing powers).

What would be true is that every theorem and proof would eventually appear, but you will never have them all (clarification: what this means is that given a theorem or a proof you can be confident that if you wait long enough at some point the computer will output it).The question is why? You won't find anything significant because of all the useless theorems and proofs.

It is similar to the idea that a computer could enumerate all images and would therefore have painted all current, past and future art. Or by having a computer go through all combinations of letters it will eventually write any story.

 

[jobyts]

The question is why? You won't find anything significant because of all the useless theorems and proofs.

It is similar to the idea that a computer could enumerate all images and would therefore have painted all current, past and future art. Or by having a computer go through all combinations of letters it will eventually write any story.

It's different from art. In art a computer cannot sort out a good picture from garbage. In case of mathematical theorems proof, a computer can clearly rule out the invalid ones. Using it to derive all the mathematical proofs will be nearly impossible. But for a given specific problem, a computer may be able to find proof for it and rule out the invalid ones.

At least we can prove that, there is no proof exist for, say Reimann hypothesis, in x number of steps. x could be in millions.

 

[rasmhop]

It's different from art. In art a computer cannot sort out a good picture from garbage. In case of mathematical theorems proof, a computer can clearly rule out the invalid ones. Using it to derive all the mathematical proofs will be nearly impossible. But for a given specific problem, a computer may be able to find proof for it and rule out the invalid ones.

For theorems it's actually a lot like art. Most theorems are worthless and the computer won't be able to rule out garbage theorems.

If you already have a statement you want to find a proof for, then it could be of some use, but it's still of limited use for the following reasons:
1) If the statement is false, then it will keep searching and you won't get any information.
2) The theorem may be undecidable in your axiom system in which case it will keep searching.
3) Even if your statement is true AND provable you have no way to know when the search will stop.

Also when you finally find a proof it will not be in an easily understandable format (200 million logical symbols is not easily readable).

Of course it could be useful once in a while, but keep in mind that this is a hypothetical scenario and we likely won't have completely automated theorem provers capable of doing anything significant by bruteforce.

At least we can prove that, there is no proof exist for, say Reimann hypothesis, in x number of steps. x could be in millions.

If there are 5 different symbols it would take 5^1000000 combinations to reach a proof of length 1 million. If the computer could go through 5^10000 combinations each nanosecond (5^10000 has ~7000 digits), then it would still take 10^33000 years to reach a proof of length 40000 symbols. Given all the short-cuts and cross-references mathematicians employ I suspect that we already have many proofs much larger than 10million symbols if they were written down explicitly.

The world's fastest supercomputer can perform almost 2*10^15 floating-point operations a second (stuff like additions and multiplications). Suppose we improved on that a 5billion-fold giving us a computer performing 10^25 floating-point operations a second. Now if somehow each floating-point operation could construct an entire combination (in reality we'd probably need at least a couple of hundreds per symbol), we can construct 10^25 combinations per second. Now suppose we collect 10 billion of these computers giving us a total power of 10^35combinations per second. Now let these run for 10billion year. This gives us 10^52 combinations, or in other words all proofs of a length up to 74 symbols. If we instead let it run 10^100 years we would get up to 203 symbols.

Asymptotically the problem just doesn't scale. By increasing the proof length by 1 symbol it takes k times longer to arrive at it where k is the number of symbols (so by going from 10 symbols to 20 symbols you would increase the time by k^10). For it to work you would need a computer that improved itself at a pretty large exponential rate. In fact it's even worse in reality as longer combinations clearly will take longer to compose. Of course in a thought experiment such a thing may exist, but in reality this doesn't work.

 

[NeoDevin]

What would be true is that every theorem and proof would eventually appear, but you will never have them all (clarification: what this means is that given a theorem or a proof you can be confident that if you wait long enough at some point the computer will output it).

Not necessarily.

 

[haael]

What would be true is that every theorem and proof would eventually appear, but you will never have them all (clarification: what this means is that given a theorem or a proof you can be confident that if you wait long enough at some point the computer will output it).

Necessarily not.

 

[rasmhop]

Not necessarily.

What do you mean?
A proof can be written as a string of symbols chosen from a finite alphabet. There are finitely many strings of n symbols for a fixed integer n, so a computer will be able to go through all combinations of length n in some time T(n). It would then take a computer.
T(1)+T(2) + \cdots+T(k)
to go through all proofs of length k or less. If it just keeps enumerating proofs, at some point we will get to arbitrarily long proofs, so any proof of finite length N will be covered in less than:
T(1)+T(2) + \cdots+T(N)
time.

On the other hand you will never have them all because a computer will only be able to through some finite number N of strings in a second (I assumed the computer had finite computing powers). So in t seconds it will at most be able to through tN strings, but there are infinitely many so there does not exist a t such that we have gone through all strings in t seconds.

 

[haael]

If it just keeps enumerating proofs, at some point we will get to arbitrarily long proofs, so any proof of finite length N will be covered

In each axiomatic system that contains arithmetics, there exist a sentence that is true, but there is no proof of it in this axiomatic system.

Here's my favorite:
Suppose we have such a model, that has natural numbers, and a predicate \phi: N -> Bool. We can now define it so that:
- For all n in N, we can proove \phi(n)
- Not for all n in N, \phi(n)

In fact, as Goedel discovered, truth and provability are different things. The set of provable sentences (in some axiomatic system) is contained in the set of true sentences, but they can not be equal, except for very simple systems.

 

[rasmhop]

In each axiomatic system that contains arithmetics, there exist a sentence that is true, but there is no proof of it in this axiomatic system.

But then it doesn't matter. I only claimed that every proof will eventually appear. I did not claim that for every true theorem we would eventually find a proof.

I now realize I also said "and every theorem" which of course is incorrect (or at least misleading). What I meant was "and every provable theorem". I made this mistake because in the original post it said "and theorems that can be derived using the axioms" and I forgot to state that I have the same requirements on theorems. Clearly we will never find a proof of a theorem that has no proof.

Sorry for the confusion.

 

[Hurkyl]

At least we can prove that, there is no proof exist for, say Reimann hypothesis, in x number of steps. x could be in millions.

You underestimate how many proofs are possible; at best, x could be dozens if we are enumerating proofs by length, if we want to see the results in our lifetime.


I feel I should point out that if you have axioms for a mathematical theory, then by definition every theorem is provable from those axioms.