Yakk wrote:I'd assume it solves the halting problem (on non-infinitely fast computers), which isn't a paradox.
So I'd write a simple proof checker and proof generator in a sufficiently powerful system.
Then I'd write the 'is provable' program, that (if something is provable) it (tells me how long the shortest proof is), and (optionally prints it out).
This would take at least a decade of work. But along the way, I'd solve at least a million dollar mathematics problem, which would keep me funded. (Only one, ideally -- and one that admits a 'counterexample' anti-proof, because I can pretend I got lucky).
The halting problem is for Turing machines, which have infinite tape memory, so the halting problem is still there; The "is provable program" can't exist , cause no matter how fast your computer can run, it will never halt. Even if you have a computer with and uncountable amount of memory, the independence of the axiom of choice shows that the halting problem in undecidable, and your "is provable program" can't exist. By definition a proof cannot be infinitely long (because the theorem is the last line of the proof), and the halting problem is equivalent to Godel's incompleteness.
M-x shell wrote:Yes, but having infinite computing power completely changes the problem. Making the proof computer-checkable is trivial, because it is computer generated. You could simply use the same rules. Now, writing a program that forms proofs would still be reasonably difficult, but nothing like trying to do so with finite computation. It isn't that hard to figure out all the things that can be done (I chose number theory because it has a fairly simple set of rules). The main challenge is pruning the tree: getting the program to investigate only the most promising possibilities. That isn't even necessary in this hypothetical scenario. It could just blindly wander the space of all possible theorems and still find the answer instantly. In practice, such a simple approach is useless, even for small proofs. But with an infinitely fast computer, you can just brute-force it.
LOL a decade of work? writing a program that forms proofs would still be reasonably difficult? haha we have a formal language that we use as for our proofs: just look at all the proofs of length 1, then all the proofs of length 2, then all the proofs of length 3, etc. Its pretty simple, and its not wandering around blindly, and it would take me 10 min to implement. It would give me a countable infinity of proofs, the last line of each proof is a theorem, and if theorem X and its converse aren't one of them, then theorem X is not provable.
Alrighht so can you tell I only read the first page of this post?
