Cook Levin library · General · Zulip Chat Archive

I’ve been trying to use AI to prove a simple theorem using the Cook Levin library - if a Turing machine outputs a certain bit at a certain location, then the Turing machine must read that bit. Chat GPT and Claude AI haven’t been able to do it. Anyone know how to do this?

Yiran Duan (Jun 18 2025 at 11:29):

I'm interested in your question as well, and just to check whether I've understood it correctly: I can prove the following lemma by simp, is it somewhat relevant to what you are proving?

Craig Alan Feinstein (Jun 20 2025 at 01:54):

Yiran, the way I understand that statement, it means "If you write symbol w to a tape without moving the head, then reading from the tape returns w". When I asked my question, I meant if the Turing machine outputs w, then beforehand it must have read bit w. To give an idea of what I had in mind, I would like to use this to prove in Isabelle that if a Turing machine take the OR function of n bits and all n bits are zero, then the Turing machine must read all of the bits beforehand.

Yiran Duan (Jun 21 2025 at 22:31):

Thank you for explaning it again! So is it something like the following (I randomly chose some tm_copy_paste as an example)?

Here's more details including my definition for tm_copy_paste and start_cfg, where I managed to prove this lemma above in my awkward way.

Scratch.thy

theory Scratch
  imports Cook_Levin.Basics
begin

text ‹"print_tape cfg n m" prints the first m symbols of n-th tape in cfg›
fun print_tape :: "config ⇒ nat ⇒ nat ⇒ symbol list" where
  "print_tape cfg n 0 = []" |
  "print_tape cfg n (Suc m) = (print_tape cfg n m) @ [(cfg <:> n) m]"

definition copy_paste_command :: command where
  "copy_paste_command = (
    λ symbols_read_from_tapes.
      (if symbols_read_from_tapes ! 0 = □ then 1 else 0, ― ‹new state›
       [(symbols_read_from_tapes ! 0, Right), ― ‹0-th tape remains the same›
        (symbols_read_from_tapes ! 0, Right)]) ― ‹copies the symbol from 0-th tape to the 1st tape›
   )"

― ‹copy_paste_command is a well-formed command for a 2-tape TM with 1 state (excluding q_f)›
lemma "wf_command 2 1 copy_paste_command"
  unfolding copy_paste_command_def
  unfolding wf_command_def
  by simp

― ‹copy_paste_command is a Turing command for a 2-tape TM with 1 state (excluding q_f),
    and with the alphabet set containing only 4 symbols (□, ▹, 𝟬, 𝟭)›
lemma cp_tm_cmd_214: "turing_command 2 1 4 copy_paste_command"
  unfolding copy_paste_command_def
  unfolding turing_command_def
  unfolding wf_command_def
  apply auto
  by (metis One_nat_def diff_Suc_1 fst_conv less_2_cases_iff nth_Cons_0 nth_Cons_numeral numerals(1))

definition tm_copy_paste :: machine where
  "tm_copy_paste = [copy_paste_command]"

― ‹The copy-paste machine is a well-formed 2-tape TM for the alphabet set of size 4›
lemma turing_machine_tm_copy_paste: "turing_machine 2 4 tm_copy_paste"
  unfolding turing_machine_def tm_copy_paste_def
  using cp_tm_cmd_214 by auto

definition start_content :: "symbol list" where
  "start_content = [𝟭, 𝟬, 𝟭, 𝟬, 𝟬, 𝟬, 𝟭, 𝟬]"

definition start_cfg :: "config" where
  "start_cfg = start_config 2 start_content"

value "print_tape start_cfg 0 10"
value "print_tape start_cfg 1 10"
value "print_tape (execute tm_copy_paste start_cfg 10) 1 10 = print_tape start_cfg 0 10"

lemma zip2: "length xs ≥ 2 ⟹ zip [a, b] xs = [(a, xs ! 0), (b, xs ! 1)]"
  apply (induction xs)
   apply auto
  by (metis Suc_le_length_iff nth_Cons_0 zip_Cons_Cons zip_Nil)

lemma aux:
  assumes "t < 10"
  shows "fst (execute tm_copy_paste start_cfg t) = 0 ∧
         (execute tm_copy_paste start_cfg t) <#> 0 = t"
  using assms
proof (induction t)
  case 0
  then show ?case
    by (simp add: start_cfg_def start_config_def)
next
  case (Suc t)
  have "□ ∉ set start_content"
    unfolding start_content_def by simp
  let ?cfg = "execute tm_copy_paste start_cfg t"
  have "||?cfg|| = 2"
    by (metis execute_num_tapes less_2_cases_iff start_cfg_def start_config_length turing_machine_tm_copy_paste)
  from Suc have IH': "fst ?cfg = 0" "?cfg <#> 0 = t"
    by simp+
  from turing_machine_tm_copy_paste
  have "?cfg <:> 0 = start_cfg <:> 0"
    by (simp add: input_tape_constant start_cfg_def start_config_length)
  with IH'(2) have "?cfg <.> 0 = (start_cfg <:> 0) t"
    by presburger
  moreover
  have "(start_cfg <:> 0) t ≠ □"
  proof (cases "t = 0")
    case True
    then show ?thesis
      by (simp add: start_cfg_def start_config2)
  next
    case False
    from ‹Suc t < 10› have "t - 1 < length start_content"
      by (simp add: start_content_def)
    with ‹□ ∉ set start_content› have "start_content ! (t - 1) ≠ □"
      by (simp add: in_set_conv_nth)
    with start_config3[where ?cfg = start_cfg and ?k = 2 and ?xs = start_content and ?i = t]
    show ?thesis
      using False ‹t - 1 < length start_content› start_cfg_def by auto
  qed
  ultimately
  have "?cfg <.> 0 ≠ □"
    by argo
  then have "config_read ?cfg ! 0 ≠ □"
    by (metis execute_num_tapes start_cfg_def start_config_length
        tapes_at_read' turing_machine_tm_copy_paste zero_less_numeral)
  then have "[*] copy_paste_command (config_read ?cfg) = 0"
    unfolding copy_paste_command_def by simp
  then have 1: "fst (sem copy_paste_command ?cfg) = 0"
    by (simp add: sem')

  from Suc have "execute tm_copy_paste start_cfg (Suc t) =
                 sem copy_paste_command ?cfg"
    by (simp add: exe_def tm_copy_paste_def)
  also have "... = (fst (sem copy_paste_command ?cfg),
                    map (λ(a, tp). act a tp) (zip (snd (copy_paste_command (read (snd ?cfg)))) (snd ?cfg)))"
    by (simp add: sem')
  also have "... = (0, map (λ(a, tp). act a tp) (zip (snd (copy_paste_command (read (snd ?cfg)))) (snd ?cfg)))"
    using 1 by blast
  also have "... = (0, map (λ(a, tp). act a tp) (zip [(?cfg <.> 0, Right), (?cfg <.> 0, Right)] (snd ?cfg)))"
    unfolding copy_paste_command_def
    by (metis (no_types, lifting) One_nat_def Suc_1 execute_num_tapes
        less_add_Suc2 plus_1_eq_Suc read_abbrev sndI start_cfg_def
        start_config_length turing_machine_tm_copy_paste)
  also have "... = (0, [act (?cfg <.> 0, Right) (?cfg <!> 0), act (?cfg <.> 0, Right) (?cfg <!> 1)])"
    using ‹||?cfg|| = 2› zip2[where ?a = "(?cfg <.> 0, Right)" and ?b = "(?cfg <.> 0, Right)" and ?xs = "snd ?cfg"]
    by simp
  also have "... = (0, [?cfg <!> 0 |+| 1, act (?cfg <.> 0, Right) (?cfg <!> 1)])"
    using act_Right by simp
  also have "... <#> 0 = Suc (?cfg <#> 0)"
    by simp
  also have "... = Suc t"
    using ‹?cfg <#> 0 = t› by blast
  finally have "execute tm_copy_paste start_cfg (Suc t) <#> 0 = Suc t" .
  moreover
  from ‹execute tm_copy_paste start_cfg (Suc t) = sem copy_paste_command ?cfg› 1
  have "fst (execute tm_copy_paste start_cfg (Suc t)) = 0"
    by presburger
  ultimately
  show ?case by blast
qed

end

Yiran Duan (Jun 21 2025 at 22:54):

Lemma aux is much stronger than (what I understood from) your statement, but I guess it provides a way to easily prove your goal. However if the ultimate goal is to prove that the turing machine terminates with some results, I think there might be better ways without having to prove such intermediate lemmas explicitly (but that's beyond my current experience with the Cook_Levin entry; I would be happy if I get the chance to learn about it in this discussion)

Craig Alan Feinstein (Jun 22 2025 at 09:43):

Yiran, It isn’t exactly what I was thinking, but it probably will be helpful. My question seems conceptually easy and obvious at first, but I couldn’t get ai to do it and it isn’t always true. What if Turing machine M prints out bit x? Then one might think M has to read bit x. But then what if it is mathematically provable that another bit y equals bit x. Then the Turing machine doesn’t have to read bit x. It could just read bit y and print it out. So there have to be extra assumptions.

Craig Alan Feinstein (Jun 22 2025 at 20:12):

Yiran, to give a better example of what I have in mind, suppose you want to determine whether there exists a nonzero x such that given square matrix A, Ax=0, where A and x are composed of zeroes and ones and we are using mod 2 arithmetic. You don’t have to check all possibilities for x to get the answer. You can do Gaussian elimination on A to see if it is non singular. In other words if you consider a bit y for each x as to whether Ax = 0 and take the or operators of these bits y you get the answer, but you don’t have to do it this way and in fact it is better that you don’t do it this way. This is why you need extra assumptions for what I’m trying to do in Isabelle to work, namely that there are no other ways of formulating the problem other than taking the or operator. Does this make sense?

Craig Alan Feinstein (Jun 23 2025 at 01:45):

Also, look up “adversary argument” as this is the type of argument that is necessary for this to work.

Craig Alan Feinstein (Jun 24 2025 at 01:24):

Another problem I just realized is that to output bit x, a Turing machine can read not x. So technically the Turing machine doesn’t have to read bit x.

Craig Alan Feinstein (Jun 24 2025 at 01:57):

Craig Alan Feinstein (Jun 27 2025 at 20:18):

A better way of phrasing it - before a Turing machine outputs bit x, it must “know” what bit x is. Similar to before a person speaks, he has to know what he is going to say.

Yiran Duan (Jul 03 2025 at 13:32):

Hi, unfortunately I still fail to understand the conversation. I try to list some points that I'm not sure with, as follows:

Are these words talking about the most brute-force method which tries all the

2^n

possibilities of x (if the matrix A in this example is of shape

n \times n

Here I am completely lost. I have no idea what "the problem" is referring to (maybe I also have doubts about what "formulating" means here).

Craig Alan Feinstein (Jul 04 2025 at 19:34):

Yiran said “Are these words talking about the most brute-force method which tries all the

2n

possibilities of x (if the matrix A in this example is of shape

n×n

)?” Yes

Craig Alan Feinstein (Jul 04 2025 at 19:42):

Yiran said “Here I am completely lost. I have no idea what "the problem" is referring to (maybe I also have doubts about what "formulating" means here).” I was saying that the matrix problem can be formulated as an “or” problem but it is not necessary to take the or operator of all 2 to the n possible solutions to determine whether there is a solution. One can just do Gaussian elimination. This is an example of an “or” problem in which it is not necessary to take the “or” operator explicitly. Hence a proof in Isabelle has to specify context of the “or” problem in order to prove that a Turing machine has to read all of the bits.

Craig Alan Feinstein (Jul 04 2025 at 19:43):

Yiran said “Does this mean "work with deterministic Turing Machines"?” I was talking about deterministic Turing machines.

Yiran Duan (Jul 09 2025 at 13:56):

I don't think I can imagine how a deterministic Turing machine "doesn't know" the bit to be output (for a given configuration). Maybe I had a different understanding of "knowing a bit"?

Craig Alan Feinstein (Jul 10 2025 at 16:10):

Yiran I would now define “knowing a bit” for a Turing machine as having the bit on the tape or the negation of the bit on the tape at a particular location. Then when the machine reads that particular location, it reads the bit or the not bit and then goes into another state in which the bit is encoded in it and then it outputs that bit.

Craig Alan Feinstein (Jul 10 2025 at 16:17):

The nuance here is to know a yes/no fact, it really doesn’t matter whether one means yes or zero means yes, as long the machine is consistent.

Yiran Duan (Jul 13 2025 at 21:03):

That would mean the machine rewrites a bit at some "particular location" with itself or its negation, right?

I tried to replace the above informal definition of "knowing a bit" (along with a transition, sharing a fixed "particular location") into this statement, and I get the following:
"Before a machine outputs x at some position head_pos, the bit at head_pos must have been x or the negation of x"
Is that what you meant, or did I misunderstood something?

Yiran Duan (Jul 13 2025 at 21:41):

Or, I guess it makes much more sense if there were actually some transitions that moves the tape head to different positions omitted; also consider working with multitape TMs, and add the constraint that contents on the first tape are never changed (which the Cook-Levin entry does), and we don't consider actions on the first tape (always rewriting with the original symbol) as an action of the machine "outputting" or "writing" something; thirdly, since we talked about bitwise or, I have always assumed that the tape alphabets only include something like 0 and 1 (and the blank symbol, or maybe also a start symbol).
In that case I would understand the goal as "when some bit x is output, it shows that x or its negation appears in the contents of the first tape (input)".
Then I must have missed something because based on this, I think it is basically to show that "if the machine ever writes a 0 or a 1 (on any tape other than the first one), the first tape must be non-empty (there is at least one 0 or 1 at any location)"?

Craig Alan Feinstein (Jul 15 2025 at 03:47):

Yiran your last comment illustrates how this problem is not as easy as it looks. You did not misunderstand me. Thinking about things more, I actually want to do the following in a proof - I want to show that in order for a Turing machine T to decide whether x = y, it is necessary for T to read both f(x) and f(y), for some one to one function f. (Assume x and y are integers.)

Craig Alan Feinstein (Jul 15 2025 at 04:10):

The proof is that if T did not read f(x) for some one to one function f, then T would behave the same way for some x’ not equal to x as it does for x. Therefore it could not decide whether x=y.

Craig Alan Feinstein (Jul 15 2025 at 16:43):

The one to one function f encodes x and y as bits that the Turing machine reads.

Stream: General

Topic: Cook Levin library

Craig Alan Feinstein (Jun 15 2025 at 17:05):