4 ms·

A Turing machine is just a computer program. The Goldbach Conjecture example is just a program to loop through and test that each successive even integer can b

by dzdt 10y ago

A Turing machine is just a computer program. The Goldbach Conjecture example is just a program to loop through and test that each successive even integer can be reached as the sum of two prime numbers. If there is a counterexample to the conjecture, then theoretically this program will eventually find it. For these purposes, the authors don't care if the program calculates efficiently, but are interested in the length of the program. So brute force is fine. The Riemann Hypothesis and ZFC programs similarly are just brute force searching for counterexamples. The existence of programs to search for counterexamples is not new or surprising. I am not so sure what part of this work is new. I guess it is the discussion of philisophical implications.

sp332 10y ago
What's new here is putting a specific upper bound on the complexity of the problem. A Turing machine using only binary symbols and at most 7,918 states is enough to prove or disprove ZFC.
- chriswarbo 10y ago
  To me, the use of Turing machines seems a little gimmicky; they're very far removed from the way we actually program, or reason about programs. The difficult problem here seems to be compilation: going from a usable program definition, either formal or informal, down to the bizarre world of Turing machines, either by hand or automatically. To me, binary combinatory logic and binary lambda calculus seem like much more sensible languages for performing these kinds of algorithmic information theory experiments.
  - sp332 10y ago
    The proof was actually written in Laconic, and then compiled down to a TM. We already know certain things about TMs (like busy beaver and the halting problem) so you don't have to re-prove those things about your new machine if you can just prove that it's equivalent to a TM. It's mainly used as a convenient way to keep score. If some other proof can be proven equivalent to a TM with fewer states, then you have a better upper bound.
  - tromp 10y ago
    Scott commented on the Turing Machine vs lambda calculus approaches in: http://www.scottaaronson.com/blog/?p=2725#comment-1085117 http://www.scottaaronson.com/blog/?p=2725#comment-1085117 showing a clear preference for the "physical" operation of Turing Machines. In the end, complexities are not that far apart, considering that https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6 https://gist.github.com/anonymous/a64213f391339236c2fe31f874... describes a 27 state Goldbach checking TM, which takes no more than 378 bits to encode, while https://github.com/tromp/AIT/blob/master/goldbach.lam https://github.com/tromp/AIT/blob/master/goldbach.lam describes an equivalent 267 bit Lambda Calculus term, which can also be represented as this https://github.com/tromp/AIT/blob/master/goldbach.gif https://github.com/tromp/AIT/blob/master/goldbach.gif lambda diagram, as explained in http://tromp.github.io/cl/diagrams.html http://tromp.github.io/cl/diagrams.html

by dzdt 10y ago

sp332 10y ago

What's new here is putting a specific upper bound on the complexity of the problem. A Turing machine using only binary symbols and at most 7,918 states is enough to prove or disprove ZFC.

chriswarbo 10y ago
To me, the use of Turing machines seems a little gimmicky; they're very far removed from the way we actually program, or reason about programs. The difficult problem here seems to be compilation: going from a usable program definition, either formal or informal, down to the bizarre world of Turing machines, either by hand or automatically. To me, binary combinatory logic and binary lambda calculus seem like much more sensible languages for performing these kinds of algorithmic information theory experiments.
- sp332 10y ago
  The proof was actually written in Laconic, and then compiled down to a TM. We already know certain things about TMs (like busy beaver and the halting problem) so you don't have to re-prove those things about your new machine if you can just prove that it's equivalent to a TM. It's mainly used as a convenient way to keep score. If some other proof can be proven equivalent to a TM with fewer states, then you have a better upper bound.
- tromp 10y ago
  Scott commented on the Turing Machine vs lambda calculus approaches in: http://www.scottaaronson.com/blog/?p=2725#comment-1085117 http://www.scottaaronson.com/blog/?p=2725#comment-1085117 showing a clear preference for the "physical" operation of Turing Machines. In the end, complexities are not that far apart, considering that https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6 https://gist.github.com/anonymous/a64213f391339236c2fe31f874... describes a 27 state Goldbach checking TM, which takes no more than 378 bits to encode, while https://github.com/tromp/AIT/blob/master/goldbach.lam https://github.com/tromp/AIT/blob/master/goldbach.lam describes an equivalent 267 bit Lambda Calculus term, which can also be represented as this https://github.com/tromp/AIT/blob/master/goldbach.gif https://github.com/tromp/AIT/blob/master/goldbach.gif lambda diagram, as explained in http://tromp.github.io/cl/diagrams.html http://tromp.github.io/cl/diagrams.html