<p>First, you don't need to turn them into Turing machines, it is essentially the same as running a proof search algorithm. The logical complexity of the formula (which in the cases you have in mind are $\Pi^0_1$) has no effect on this, searching for proofs in any effective theory (like ZFC, for proof to make sense you have to fix a theory) can be done in a straight forward manner, the set of provable statements for any effective theory is $\Sigma^0_1$ and therefore computable enumerable.  But there are no reasons to do that, you don't gain anything a priori just by adding one extra unnecessary layer of coding, it has no benefit (AFAIK).</p>

<p>Also don't confuse proof search with a direct reduction from the truth of a $\Pi^0_1$ statement to the halting problem (which exists as not halting is $\Pi^0_1$-complete).</p>

<p>Second, consider the much simpler case of <em>propositional</em> tautologies in place of first-order statements like GC. (propositional tautologies is a coNP set also known as $\Pi^B_1$). The state of art proof search algorithms (i.e. SAT solvers) are exponentially inefficient in finding proofs of very simple finitary mathematical statements like the pigeon-hole principle tautologies. You can run a first-order proof search program to look for a ZFC proof of GC but I haven't seen <em>any</em> interesting mathematical statement being discovered/proven by unguided brute-force search of proofs. So there is no example of this being useful. (For human-guided use of computer in proving mathematical theorems we have the four colors theorem.)</p>

<p>Third, if you use a proof search algorithm you will only know if there is a proof, if there isn't any you will not know and the algorithm will continue forever without halting. In other words, you can't write a program like the one you have stated in the question (which is why I commented that this is more suitable for CS Q&amp;A site since this is very basic mistake in computability theory).</p>

<p>See also my answers to similar questions on <a href="https://math.stackexchange.com/questions/156975/solving-p-vs-np-with-computer/157493#157493">math</a> and <a href="https://cs.stackexchange.com/questions/7737/is-it-mathsfnp-hard-to-decide-whether-mathsfp-mathsfnp/7774#7774">CS</a>.</p>

CC BY-SA 3.0
2014-02-19T16:24:23.280Z
following [se popular convention](http://meta.stackexchange.com/questions/135/encouraging-people-to-explain-downvotes): in busy beaver research, which admittedly started out more as a "toy" type problem as in its whimsical naming, but which has significantly advanced over many years, there are many TMs that have been _proven_ to be nonhalting, but for which these proofs have never been converted to any other proof systems in the literature. it is certainly true that equivalent proofs _could be_ constructed in other proof systems. also, sometimes misc problems are solved via "bridge thms" etc
vzn
CC BY-SA 3.0
2014-02-16T11:26:27.447Z
2014-02-17T15:03:49.243Z
2017-04-13T12:48:30.830Z
Kaveh
<p>Lets assume the proof of a conjecture, for example, the famous Goldbach conjecture. Is it possible to try to prove or disprove such a conjecture by devising a Turing machine that accepts if the proof is possible.
So, for Turing machine M, </p>

<p>If, the conjecture is provable, accept, else reject.</p>

<p>So, in essence, we don't try to find a proof of the conjecture, but, try to find whether its provable, something like zero-knowledge proofs. </p>

<p><strong>Additional Details</strong>:
I felt the way most of these conjectures go, is they say: For all n, C holds true. 
So, in essence, even if it can be shown that C holds up to some n, but, it hasn't been able to be derived for all n. And, this seems to bear a striking similarity to the Halting problem. So, I felt a mapping must be worthwhile to study/research.</p>

CC BY-SA 3.0
2014-02-16T08:13:35.407Z
A) It's not clear to me if achieving this goal would help anyway... (is proving that $P$ is provable as hard as proving $P$?). B) My own instinct is the TM approach is very unlikely to help, because we know that in general reasoning about TMs/halting/accepting/rejecting is hard. So you need to encode a lot of the structure of your problem into the algorithm somehow (compare to a universal prover that searches for the proof/disproof of any given theorem...we can show nothing about this). C) Perhaps a good question is "Are there any known cases of this technique working?"
usul
CC BY-SA 3.0
2014-02-16T11:39:12.327Z
I think this question is more suitable for [cs.se]. Also I don't see any relation with zero-knowledge proof systems.
Kaveh
CC BY-SA 3.0
2014-02-16T11:51:50.493Z
Hmm, I realize that I interpreted your question as asking whether we could gain insight by analyzing the TM we've designed. But perhaps you are just asking about *running* it? (In which case you would probably rather use *e.g.* Coq or Agda....)
usul
CC BY-SA 3.0
2014-02-16T15:39:07.777Z
to me this is highly worthwhile/meaningful _research_ & actually have done exactly this re collatz conjecture, but there is no _immediate_ chance of success because even small TMs can barely be analyzed by existing "technology"... it would have to be seen as a very longterm research program; there are other very longterm type programs in CS eg "geometric complexity theory". but it requires an _inspiring leader_ to trigger those types of efforts... would like to answer your question with refs but am gonna hold off until there are votes, which suspect will very likely _not_ materialize **=(**
vzn
CC BY-SA 3.0
2014-02-16T16:36:17.233Z
@vzn , can you please cite some references that might guide me in the right direction? I am very interested to know how much progress has been made in this field?
saikat
CC BY-SA 3.0
2014-02-16T17:53:59.063Z
hi user1951547, "progress" is extremely limited in this area due to it being a _very hard_ unified/crosscutting theory/challenge spanning both deep TCS/math. closest line of research is prob on [busy beavers](http://en.wikipedia.org/wiki/Busy_beaver) with some modest results so far & [continuing] work in that area. am planning on writing a blog on it with the collected refs & scattered se questions on subj/line of research also. after you earn 20pt rep somewhere on se can [chat] about it further.
vzn
CC BY-SA 3.0
2014-02-17T16:27:29.077Z
@vzn Why would you wait for votes to write an answer? It's not money. Weird.
AndrewC
CC BY-SA 3.0
2014-02-17T18:56:59.703Z
AC votes are a sometimes very accurate measure of group interest in the question/problem (ie dynamically identified "topic scope") & do in fact function in many ways like a virtual/informal currency/exchange system eg with bounties etc. ... more of a meta topic. ... anyway the question is now rescued from a split with new votes & may venture an answer at some pt now. as for your strawman implication below to the poster as someone who hasnt studied it & whether this line of inquiry is in scope on a **TCS research site,** that is inappropriate sarcasm here & disrespectful imho, ie **not nice**
vzn
CC BY-SA 3.0
2014-02-17T19:21:35.590Z
@vzn Straw man is where you misrepresent a point in order to attack it. I was disagreeing with your "many great examples of this from theoretical math/TCS & in many ways this phenomenon lies at the heart of progress": hyperbole all yours, no need for me to exaggerate or misrepresent you. Most progress _isn't_ from "bridge theorems", and the _big_ results don't originate on SE. I'm not claiming it's off topic, it's just you seemed to feel the question is on the brink of some great discovery, but I really didn't get that impression, and was pointing out that suchlike are usually hard fought for.
AndrewC
CC BY-SA 3.0
2014-02-18T01:29:14.693Z
This question is either very subjective ("is it worthwhile") or very basic ("is it possible"). In either case I do not think it's a good question for this site.
Sasho Nikolov
CC BY-SA 3.0
2014-02-18T02:47:25.957Z
SN how does a researcher determine what is worthwhile? there would be very few refs addressing that very significant/monumental research issue (although maybe thats more a [tag:soft-question] or [tag:big-picture] type question, also this question seems to fit [tag:application-of-theory]...) as for whether it is possible, why do you think that is basic?
vzn
CC BY-SA 3.0
2014-02-18T05:04:42.427Z
figuring out whether something is worthwhile is an important skill, but there is no right answer to this question, except in hindsight. that is why it is not an appropriate question for cstheory imo. also the question is hard to understand because it is very vague (e.g. how do you "assume the proof of GC", what does this have to do with ZKP, etc.) as to the basic confusions about computability and logic, see Kaveh's answer.
Sasho Nikolov
CC BY-SA 3.0
2014-02-18T05:18:19.557Z
It may be worth OP's time to read this post by Terry Tao: https://plus.google.com/114134834346472219368/posts/cy6KB8TKMkA. Posing a problem in a new language is only useful if it opens a new perspective on the structure of the problem and/or gives access to powerful tools. TMs are general enough to "reduce" almost any statement to a statement about whether a particular TM halts. But I don't see how that is a useful reduction in either of the two senses above.
Sasho Nikolov
CC BY-SA 3.0
2014-02-18T19:11:03.027Z
ok more on [mounting or solving open problems/research programs](http://rjlipton.wordpress.com/2012/12/08/mounting-or-solving-open-problems/) RJL. actually a twist: lately am thinking a highly novel yet similar idea called [SAT induction](http://vzn1.wordpress.com/2014/02/14/great-moments-in-empiricalexperimental-mathtcs-research-breakthough-sat-induction-idea/) (there is a basic interconnection in the sense of problem → TM → SAT instances) may be more fundamental/promising than the partial approach being considered on this question; lots of refs/leads/circumstantial evidence given on that pg
vzn
CC BY-SA 3.0
2014-02-23T02:42:09.773Z
@SashoNikolov you should consider turning your comment with the Terry Tao link into an answer. It is a great soft-answer to this question.
Artem Kaznatcheev
<turing-machines><proofs>
Is it worthwhile to try to prove a conjecture by mapping it to a Turing machine?
saikat
# Is it worthwhile to try to prove a conjecture by mapping it to a Turing machine?

(Asked by: username_0 on 2014-02-16)

Lets assume the proof of a conjecture, for example, the famous Goldbach conjecture. Is it possible to try to prove or disprove such a conjecture by devising a Turing machine that accepts if the proof is possible.
So, for Turing machine M,

If, the conjecture is provable, accept, else reject.

So, in essence, we don't try to find a proof of the conjecture, but, try to find whether its provable, something like zero-knowledge proofs.

**Additional Details**:
I felt the way most of these conjectures go, is they say: For all n, C holds true.
So, in essence, even if it can be shown that C holds up to some n, but, it hasn't been able to be derived for all n. And, this seems to bear a striking similarity to the Halting problem. So, I felt a mapping must be worthwhile to study/research.

**Tags:** turing-machines, proofs
> **Comments:**
> **username_1**: A) It's not clear to me if achieving this goal would help anyway... (is proving that $P$ is provable as hard as proving $P$?). B) My own instinct is the TM approach is very unlikely to help, because we know that in general reasoning about TMs/halting/accepting/rejecting is hard. So you need to encode a lot of the structure of your problem into the algorithm somehow (compare to a universal prover that searches for the proof/disproof of any given theorem...we can show nothing about this). C) Perhaps a good question is "Are there any known cases of this technique working?"  
> **username_2**: I think this question is more suitable for [cs.se]. Also I don't see any relation with zero-knowledge proof systems.  
> **username_1**: Hmm, I realize that I interpreted your question as asking whether we could gain insight by analyzing the TM we've designed. But perhaps you are just asking about *running* it? (In which case you would probably rather use *e.g.* Coq or Agda....)  
> **username_3**: to me this is highly worthwhile/meaningful _research_ & actually have done exactly this re collatz conjecture, but there is no _immediate_ chance of success because even small TMs can barely be analyzed by existing "technology"... it would have to be seen as a very longterm research program; there are other very longterm type programs in CS eg "geometric complexity theory". but it requires an _inspiring leader_ to trigger those types of efforts... would like to answer your question with refs but am gonna hold off until there are votes, which suspect will very likely _not_ materialize **=(**  
> **username_0**: @vzn , can you please cite some references that might guide me in the right direction? I am very interested to know how much progress has been made in this field?  
> **username_3**: hi user1951547, "progress" is extremely limited in this area due to it being a _very hard_ unified/crosscutting theory/challenge spanning both deep TCS/math. closest line of research is prob on [busy beavers](http://en.wikipedia.org/wiki/Busy_beaver) with some modest results so far & [continuing] work in that area. am planning on writing a blog on it with the collected refs & scattered se questions on subj/line of research also. after you earn 20pt rep somewhere on se can [chat] about it further.  
> **username_4**: @vzn Why would you wait for votes to write an answer? It's not money. Weird.  
> **username_3**: AC votes are a sometimes very accurate measure of group interest in the question/problem (ie dynamically identified "topic scope") & do in fact function in many ways like a virtual/informal currency/exchange system eg with bounties etc. ... more of a meta topic. ... anyway the question is now rescued from a split with new votes & may venture an answer at some pt now. as for your strawman implication below to the poster as someone who hasnt studied it & whether this line of inquiry is in scope on a **TCS research site,** that is inappropriate sarcasm here & disrespectful imho, ie **not nice**  
> **username_4**: @vzn Straw man is where you misrepresent a point in order to attack it. I was disagreeing with your "many great examples of this from theoretical math/TCS & in many ways this phenomenon lies at the heart of progress": hyperbole all yours, no need for me to exaggerate or misrepresent you. Most progress _isn't_ from "bridge theorems", and the _big_ results don't originate on SE. I'm not claiming it's off topic, it's just you seemed to feel the question is on the brink of some great discovery, but I really didn't get that impression, and was pointing out that suchlike are usually hard fought for.  
> **username_5**: This question is either very subjective ("is it worthwhile") or very basic ("is it possible"). In either case I do not think it's a good question for this site.  
> **username_3**: SN how does a researcher determine what is worthwhile? there would be very few refs addressing that very significant/monumental research issue (although maybe thats more a [tag:soft-question] or [tag:big-picture] type question, also this question seems to fit [tag:application-of-theory]...) as for whether it is possible, why do you think that is basic?  
> **username_5**: figuring out whether something is worthwhile is an important skill, but there is no right answer to this question, except in hindsight. that is why it is not an appropriate question for cstheory imo. also the question is hard to understand because it is very vague (e.g. how do you "assume the proof of GC", what does this have to do with ZKP, etc.) as to the basic confusions about computability and logic, see Kaveh's answer.  
> **username_5**: It may be worth OP's time to read this post by Terry Tao: https://plus.google.com/114134834346472219368/posts/cy6KB8TKMkA. Posing a problem in a new language is only useful if it opens a new perspective on the structure of the problem and/or gives access to powerful tools. TMs are general enough to "reduce" almost any statement to a statement about whether a particular TM halts. But I don't see how that is a useful reduction in either of the two senses above.  
> **username_3**: ok more on [mounting or solving open problems/research programs](http://rjlipton.wordpress.com/2012/12/08/mounting-or-solving-open-problems/) RJL. actually a twist: lately am thinking a highly novel yet similar idea called [SAT induction](http://vzn1.wordpress.com/2014/02/14/great-moments-in-empiricalexperimental-mathtcs-research-breakthough-sat-induction-idea/) (there is a basic interconnection in the sense of problem → TM → SAT instances) may be more fundamental/promising than the partial approach being considered on this question; lots of refs/leads/circumstantial evidence given on that pg  
> **username_6**: @SashoNikolov you should consider turning your comment with the Terry Tao link into an answer. It is a great soft-answer to this question.  

---

## 1 answers

### Answer by username_2 on 2014-02-16. Score: 6

First, you don't need to turn them into Turing machines, it is essentially the same as running a proof search algorithm. The logical complexity of the formula (which in the cases you have in mind are $\Pi^0\_1$) has no effect on this, searching for proofs in any effective theory (like ZFC, for proof to make sense you have to fix a theory) can be done in a straight forward manner, the set of provable statements for any effective theory is $\Sigma^0\_1$ and therefore computable enumerable. But there are no reasons to do that, you don't gain anything a priori just by adding one extra unnecessary layer of coding, it has no benefit (AFAIK).

Also don't confuse proof search with a direct reduction from the truth of a $\Pi^0\_1$ statement to the halting problem (which exists as not halting is $\Pi^0\_1$-complete).

Second, consider the much simpler case of *propositional* tautologies in place of first-order statements like GC. (propositional tautologies is a coNP set also known as $\Pi^B\_1$). The state of art proof search algorithms (i.e. SAT solvers) are exponentially inefficient in finding proofs of very simple finitary mathematical statements like the pigeon-hole principle tautologies. You can run a first-order proof search program to look for a ZFC proof of GC but I haven't seen *any* interesting mathematical statement being discovered/proven by unguided brute-force search of proofs. So there is no example of this being useful. (For human-guided use of computer in proving mathematical theorems we have the four colors theorem.)

Third, if you use a proof search algorithm you will only know if there is a proof, if there isn't any you will not know and the algorithm will continue forever without halting. In other words, you can't write a program like the one you have stated in the question (which is why I commented that this is more suitable for CS Q&A site since this is very basic mistake in computability theory).

See also my answers to similar questions on [math](https://math.stackexchange.com/questions/156975/solving-p-vs-np-with-computer/157493#157493) and [CS](https://cs.stackexchange.com/questions/7737/is-it-mathsfnp-hard-to-decide-whether-mathsfp-mathsfnp/7774#7774).

> **Comments:**
> **username_3**: following [se popular convention](http://meta.stackexchange.com/questions/135/encouraging-people-to-explain-downvotes): in busy beaver research, which admittedly started out more as a "toy" type problem as in its whimsical naming, but which has significantly advanced over many years, there are many TMs that have been _proven_ to be nonhalting, but for which these proofs have never been converted to any other proof systems in the literature. it is certainly true that equivalent proofs _could be_ constructed in other proof systems. also, sometimes misc problems are solved via "bridge thms" etc  

---

