27-state Turing machine and Goldbach's conjecture

Stream: general

[Yijun Leng]

• I verified a 27-state Turing machine which halts if, and only if, Goldbach's conjecture is false
• This turing machine is originally proposed by code golf addict
• My motivation is that, wiki says

• A 43-state Turing machine has been constructed that halts if, and only if, Goldbach's conjecture is false, and a 27-state machine for that conjecture has been proposed but not yet verified.

• Now it should be modified to

• A 43-state Turing machine has been constructed that halts if, and only if, Goldbach's conjecture is false, and a 27-state machine for that conjecture has been proposed and verified in lean4.

• This is not a difficult job, but it's interesting.

• https://github.com/lengyijun/goldbach_tm

Update: Actually, it's a 26-state Turing machine : 22 and 24 are same state.

Update 2: Now 25 states is enough

[Floris van Doorn]

Nice!
Is that the smallest Turing Machine whose halting problem is equivalent to a (famous) mathematical conjecture not formulated using Turing Machines?

[Ruben Van de Velde]

And does it halt? :innocent:

[Kevin Buzzard]

No.

[Kevin Buzzard]

Although I haven't verified my answer

[Bhavik Mehta]

Floris van Doorn said:

Nice!
Is that the smallest Turing Machine whose halting problem is equivalent to a (famous) mathematical conjecture not formulated using Turing Machines?

Famous is debatable here, but there's a 15-state Turing machine which halts if and only if an old conjecture of Erdős holds: "for n > 8, there is at least one digit 2 in the base-3 representation of 2^n".

[Kevin Buzzard]

FWIW I've heard of that conjecture, and even computed a bunch of examples once many years ago. It's a great conjecture because it's so obvious that given a random large string of 0,1,2's, there will be a 2 :-)

$ gp
Reading GPRC: /etc/gprc
GPRC Done.

                  GP/PARI CALCULATOR Version 2.15.4 (released)
? digits(2^8,3)
%1 = [1, 0, 0, 1, 1, 1]

[Edward van de Meent]

who said anything about random

[Joachim Breitner]

Yijun Leng said:

• Now it should be modified to …

May be I am missing something, but why even still mention the unverified 43-state machine if we have a 27 state machine that’s verified?

[Joseph Myers]

A more general version of that conjecture (discussed several times on the Seqfan mailing list, going back at least to 1999) is: let a and b be positive integers, neither a rational power of the other. Let S be a set of natural numbers such that their base-a expansions form a regular language, and let T be a set of natural numbers such that their base-b expansions form a regular language. Suppose the densities of S and T are such that you would expect them (if random) to have finite intersection. Then S and T do have finite intersection.

[Alex Meiburg]

Joachim Breitner said:

May be I am missing something, but why even still mention the unverified 43-state machine if we have a 27 state machine that’s verified?

The 43-state one was verified. After digging a bit through Scott's comments, the "verified" meant:

No, we only meant “verified” in the physics sense—i.e., Adam communicated with the authors, understood what in the machine’s behavior was supposed to correspond to generating the primes, searching for Goldbach counterexamples, etc., and then checked in a simulator that the machine actually had that behavior.

So, a decently thorough peer-review. The 27-state hadn't been independently verified by anyone to a meaningful extent, really, it seems.

[Mario Carneiro]

"we tested empirically by adding spurious goldbach counterexamples to the integers, that the machine was able to pick them up"

[Alex Meiburg]

I've edited the Wikipedia article appropriately. :)

[Mario Carneiro]

@Yijun Leng BTW you can shorten those forward h chains using iterate 10 forward h

[Yijun Leng]

Mario Carneiro said:

Yijun Leng BTW you can shorten those forward h chains using iterate 10 forward h

Updated, thx

[Kevin Buzzard]

Alex Meiburg said:

I've edited the Wikipedia article appropriately. :)

Is the lean Zulip regarded as a reliable secondary source by Wikipedia??

[Ruben Van de Velde]

Well, "This article has multiple issues."

[Alex Meiburg]

I didn't cite Zulip, just the GitHub. But Wikipedia regularly has e.g. statements cited with only an arxiv e-print (pre-print?). This isn't ideal, but I also don't think it's really a contentious thing to claim, esp. given that the previous statements are just "this mathematician said he checked and it seemed good". So my impression is that this is a perfectly fine citation for the matter.

If/when there's some secondary source writing about it, that would be a good additional citation, certainly.

[Ruben Van de Velde]

One could submit a blog post to the lean community blog :innocent:

[Alex Meiburg]

Is that something Yijun would be expected to write, as the sole author of the formalization, or would it be someone else commenting on it? If the latter, I would be happy to, I think this is pretty neat.

[Ruben Van de Velde]

I guess it would be courteous to at least talk to them

[Yijun Leng]

Update : Actually, it's a 26-state Turing machine : 22 and 24 are same state.

In lean, we can verify that immediately

[Jz Pan]

What about https://en.wikipedia.org/wiki/Perfect_number#Odd_perfect_numbers, can it have states fewer than 15?

[Martin Dvořák]

Mario Carneiro said:

"we tested empirically by adding spurious goldbach counterexamples to the integers, that the machine was able to pick them up"

How can it possibly be done?

[Daniel Weber]

I think that's a joke

[Yijun Leng]

Update 2 : Now 25 states is enough

By eliminating unreachable case

How to reduce 26 states to 25 states

[Yijun Leng]

Jz Pan said:

What about https://en.wikipedia.org/wiki/Perfect_number#Odd_perfect_numbers, can it have states fewer than 15?

I guess 15 is not enough

[Yijun Leng]

Floris van Doorn said:

Nice!
Is that the smallest Turing Machine whose halting problem is equivalent to a (famous) mathematical conjecture not formulated using Turing Machines?

More interesting turing machines here: https://wiki.bbchallenge.org/wiki/Cryptids

I think some of are not so difficult

[Kevin Buzzard]

Some of these Collatz-like questions are undecidable (because you can simulate a Turing machine with a Collatz-like question, this is what FRACTRAN does). When I read Conway's paper on the matter I came away thinking that the Collatz conjecture itself could well be undecidable (and hence lost interest in it).