3 ms·

I'm not sure: doesn't the halting problem apply to this? In other words, can you write such a brute force program that is guaranteed to halt after a finite numb

I'm not sure: doesn't the halting problem apply to this? In other words, can you write such a brute force program that is guaranteed to halt after a finite number of steps, providing a yes or no? I guess not.

Ar-Curunir 10y ago
You just look for all proofs of a certain length. This is equivalent to checking if a Turing machine halts within a bounded number of steps. This is a NP problem.
hyperpape 10y ago
It doesn't, and it's interesting why. You can enumerate all possible proofs. If there is a proof of a given statement, you will eventually find it. But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. For the same reason, for any program that halts, you can run it long enough, and see that it halts. But (unless you are lucky enough to detect a loop), if it doesn't halt, you will never witness that, you will only be able to say "it hasn't halted yet". It definitely can take a while until that kind of asymmetry becomes intuitive.
- jerf 10y ago
  There's also the problem of identifying a proof when you have it. Hooray, after running a super-exponential number of steps in the real universe somehow it turns out Turing Machine #38,384,768,209,040,100 halts after fifteen googleplex and change steps. What does that mean? (This is not criticism, this is elaboration. The approach is useless in practice, but deeply understanding all the reasons why is a good exercise in computer science.)
- ifdefdebug 10y ago
  > But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. But that's exactly what I meant. So the brute force program proposed in the post I replied to doesn't exist, right? Let's say, you have proposition A. You write a program to brute force proofs for A. If it finds a proof, it will halt and output Yes, if it finds a disproof it will halt and output No, otherwise it will check the next proof. So if you say that your brute force program can proof/disproof proposition A (and A1, A2, A3, ... for that matter), you will have to proof that your program will halt for sure after a finite number of steps. Now that's proposition B. If you find a clever proof for proposition B, then you can claim that you wrote a program that can proof or disproof proposition A - maybe in a zillion years, but it can. If you can't find such a proof for proposition B, you can always try to write a brute force program to proof/disproof proposition B... then C, D, E, etc. :) And here comes the halting problem: you may be able to proof that a specific program will halt on a specific input, but it can be very hard to proof. But you can't proof that a specific program will halt on every input. This is directly related to Godel's incompleteness of formal systems.
  - Certhas 10y ago
    Every conjecture that is provable can be proved by the proposed program of length (conjecture + constant) in finite time. That was the original statement: > you can encode any proof to a few hundred lines. This type of encoding is funny of course. You can not determine from the encoding of the proof whether the encoding is the encoding of a proof (as you point out). But if you have a proof, and thus know that a proof exists you can "encode" it very succinctly in this program for whatever that is worth.
    - ifdefdebug 10y ago
      > you can encode any proof to a few hundred lines. Yeah, I misread that. The sentence implies the existence of a proof. So I was clearly talking about something different. Thanks.
deleted 10y ago
[deleted]
sp332 10y ago
This was an issue in another recent story. https://news.ycombinator.com/item?id=11676918 https://news.ycombinator.com/item?id=11676918 The incompleteness theorem bites you before the halting problem does.
bweitzman 10y ago
You are not trying to prove the thing, just trying to encode it, The assumption is that the proof already exists.

Ar-Curunir 10y ago

You just look for all proofs of a certain length. This is equivalent to checking if a Turing machine halts within a bounded number of steps. This is a NP problem.

hyperpape 10y ago

It doesn't, and it's interesting why. You can enumerate all possible proofs. If there is a proof of a given statement, you will eventually find it. But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. For the same reason, for any program that halts, you can run it long enough, and see that it halts. But (unless you are lucky enough to detect a loop), if it doesn't halt, you will never witness that, you will only be able to say "it hasn't halted yet". It definitely can take a while until that kind of asymmetry becomes intuitive.

jerf 10y ago
There's also the problem of identifying a proof when you have it. Hooray, after running a super-exponential number of steps in the real universe somehow it turns out Turing Machine #38,384,768,209,040,100 halts after fifteen googleplex and change steps. What does that mean? (This is not criticism, this is elaboration. The approach is useless in practice, but deeply understanding all the reasons why is a good exercise in computer science.)
ifdefdebug 10y ago
> But if there is no proof, you will never know, because it always could be the next proof you haven't looked at. But that's exactly what I meant. So the brute force program proposed in the post I replied to doesn't exist, right? Let's say, you have proposition A. You write a program to brute force proofs for A. If it finds a proof, it will halt and output Yes, if it finds a disproof it will halt and output No, otherwise it will check the next proof. So if you say that your brute force program can proof/disproof proposition A (and A1, A2, A3, ... for that matter), you will have to proof that your program will halt for sure after a finite number of steps. Now that's proposition B. If you find a clever proof for proposition B, then you can claim that you wrote a program that can proof or disproof proposition A - maybe in a zillion years, but it can. If you can't find such a proof for proposition B, you can always try to write a brute force program to proof/disproof proposition B... then C, D, E, etc. :) And here comes the halting problem: you may be able to proof that a specific program will halt on a specific input, but it can be very hard to proof. But you can't proof that a specific program will halt on every input. This is directly related to Godel's incompleteness of formal systems.
- Certhas 10y ago
  Every conjecture that is provable can be proved by the proposed program of length (conjecture + constant) in finite time. That was the original statement: > you can encode any proof to a few hundred lines. This type of encoding is funny of course. You can not determine from the encoding of the proof whether the encoding is the encoding of a proof (as you point out). But if you have a proof, and thus know that a proof exists you can "encode" it very succinctly in this program for whatever that is worth.
  - ifdefdebug 10y ago
    > you can encode any proof to a few hundred lines. Yeah, I misread that. The sentence implies the existence of a proof. So I was clearly talking about something different. Thanks.

deleted 10y ago

[deleted]

sp332 10y ago

This was an issue in another recent story. https://news.ycombinator.com/item?id=11676918 https://news.ycombinator.com/item?id=11676918 The incompleteness theorem bites you before the halting problem does.

bweitzman 10y ago

You are not trying to prove the thing, just trying to encode it, The assumption is that the proof already exists.