Import 21-state Goldbach Turing machine semantics

LeanPool/CryptidsGoldbach.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2026 Google LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maxence Faldor, Moritz Firsching
+-/
+module
+
+public import LeanPool.CryptidsGoldbach.Semantics
+
+/-!
+# A 21-state Turing machine for Goldbach's conjecture
+
+Source: url:https://github.com/google-deepmind/cryptids/tree/f873434871b2301d5c8c91ba6fa224f92c93c1e1
+Authors: Maxence Faldor, Moritz Firsching
+Status: verified
+Main declarations: `ConjectureMachines.Goldbach21.Semantics.halts_candidate_iff_not_goldbach`
+Tags: computability, turing-machines, goldbach-conjecture, machine-simulation
+MSC: 03D10, 11P32
+-/
+
+/-!
+# A 21-state Goldbach Turing machine
+
+Adapted from google-deepmind/cryptids at f873434871b2301d5c8c91ba6fa224f92c93c1e1.
+The imported scope is the complete Goldbach proof and its finite-machine infrastructure.
+The Riemann, ZF and Busy Beaver developments are outside this project.
+-/

LeanPool/CryptidsGoldbach/Imports.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.CryptidsGoldbach
+public import LeanPool.CryptidsGoldbach.Goldbach21
+public import LeanPool.CryptidsGoldbach.Machines
+public import LeanPool.CryptidsGoldbach.Propositions
+public import LeanPool.CryptidsGoldbach.Semantics

LeanPool/CryptidsGoldbach/Machines.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2026 Google LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maxence Faldor, Moritz Firsching
+-/
+module
+
+public import Mathlib.Computability.TuringMachine.Tape
+public import Mathlib.Computability.StateTransition
+
+/-!
+# Finite-state Turing machines
+
+A machine has a finite transition table and a tape from Mathlib. This module preserves
+the execution definitions and the two Goldbach tables from google-deepmind/cryptids.
+The tables are embedded as Lean literals so importing the project needs no external files.
+-/
+
+@[expose] public section
+namespace ConjectureMachines
+open Turing StateTransition
+
+/-- A transition table: for a state and the symbol under the head, either the
+symbol to write, the direction to move and the state to enter, or `none` to
+halt. -/
+structure Machine (states symbols : ℕ) where
+  /-- The action for each state and scanned symbol. -/
+  transition : Fin states → Fin symbols → Option (Fin symbols × Dir × Fin states)
+
+variable {states symbols : ℕ} [NeZero states] [NeZero symbols]
+
+/-- A configuration: the current state and the tape, whose `head` is the
+symbol under the head. -/
+structure Cfg (states symbols : ℕ) [NeZero symbols] where
+  /-- The current control state. -/
+  state : Fin states
+  /-- The tape and head position. -/
+  tape : Tape (Fin symbols)
+
+/-- One step, or `none` when the transition is missing. -/
+def step (M : Machine states symbols) : Cfg states symbols → Option (Cfg states symbols)
+  | ⟨q, T⟩ => (M.transition q T.head).map fun ⟨a, d, q'⟩ => ⟨q', (T.write a).move d⟩
+
+/-- The start state on the all-blank tape. -/
+def init : Cfg states symbols := ⟨0, Tape.mk₁ []⟩
+
+/-- `M` halts when started in state `0` on the all-blank tape. -/
+def Halts (M : Machine states symbols) : Prop := (StateTransition.eval (step M) init).Dom
+
+/-- Build a `Machine states symbols` from a list of per-state transition rows. -/
+def Machine.ofRows (rows : List (List (Option (Fin symbols × Dir × Fin states)))) :
+    Machine states symbols := ⟨fun q a => (rows.getD q.val []).getD a.val none⟩
+
+/-- A Turing machine over `symbols` tape symbols bundled with its non-zero state count. -/
+structure BundledMachine (symbols : ℕ) where
+  /-- The number of control states. -/
+  states : ℕ
+  [neZeroStates : NeZero states]
+  /-- The transition table with this state count. -/
+  toMachine : Machine states symbols
+
+attribute [instance] BundledMachine.neZeroStates
+
+/-- Bundle a `Machine (states + 1) symbols` into a `BundledMachine symbols`. -/
+abbrev Machine.bundle {states symbols : ℕ} (M : Machine (states + 1) symbols) :
+    BundledMachine symbols := ⟨states + 1, M⟩
+
+/-- `M` halts when started in state `0` on the all-blank tape. -/
+abbrev BundledMachine.Halts {symbols : ℕ} [NeZero symbols] (M : BundledMachine symbols) : Prop :=
+  ConjectureMachines.Halts M.toMachine
+
+export BundledMachine (Halts)
+
+namespace Machines
+
+/-- Rows of the 25-state machine of Yijun Leng, from the upstream baseline table. -/
+def goldbach25Rows : List (List (Option (Fin 2 × Dir × Fin 25))) := [
+  [some (1, .right, 1), some (1, .right, 3)],
+  [some (1, .left, 2), some (1, .right, 1)],
+  [some (0, .right, 0), some (1, .left, 2)],
+  [some (0, .left, 16), some (1, .right, 4)],
+  [some (0, .left, 5), some (1, .right, 6)],
+  [some (0, .left, 2), some (1, .left, 5)],
+  [some (0, .left, 5), some (0, .left, 7)],
+  [some (1, .left, 16), some (1, .left, 8)],
+  [some (0, .right, 9), some (0, .left, 8)],
+  [some (1, .right, 10), some (0, .left, 9)],
+  [some (0, .right, 11), some (0, .right, 18)],
+  [some (1, .right, 11), some (0, .right, 12)],
+  [some (1, .right, 13), some (1, .right, 12)],
+  [some (0, .left, 14), some (0, .left, 20)],
+  [some (0, .left, 15), some (1, .left, 14)],
+  [some (1, .right, 7), some (1, .left, 23)],
+  [some (1, .left, 17), some (1, .left, 16)],
+  [some (0, .right, 10), some (0, .left, 19)],
+  [some (1, .left, 17), some (1, .right, 18)],
+  [none, some (1, .right, 2)],
+  [some (1, .left, 21), some (1, .left, 20)],
+  [some (0, .left, 22), some (0, .left, 9)],
+  [some (0, .right, 10), some (0, .left, 22)],
+  [some (1, .right, 24), some (1, .left, 23)],
+  [some (1, .right, 4), some (1, .right, 24)]
+]
+
+/-- The 25-state Goldbach baseline. -/
+def goldbach25 : Machine 25 2 := Machine.ofRows goldbach25Rows
+
+/-- Rows of the 21-state machine of Maxence Faldor and Moritz Firsching. -/
+def goldbach21Rows : List (List (Option (Fin 2 × Dir × Fin 21))) := [
+  [some (1, .left, 9), some (0, .right, 5)],
+  [some (0, .right, 9), some (1, .right, 3)],
+  [some (1, .right, 15), some (1, .left, 2)],
+  [none, some (1, .right, 4)],
+  [some (0, .left, 14), some (1, .right, 6)],
+  [some (1, .left, 16), some (1, .right, 5)],
+  [some (0, .right, 7), some (0, .left, 7)],
+  [some (0, .left, 12), some (1, .left, 20)],
+  [some (1, .right, 1), some (0, .left, 8)],
+  [some (1, .right, 9), some (0, .right, 10)],
+  [some (1, .right, 11), some (1, .right, 10)],
+  [some (0, .left, 12), some (0, .left, 18)],
+  [some (1, .left, 13), some (1, .left, 12)],
+  [some (1, .left, 14), some (0, .left, 2)],
+  [some (1, .left, 16), some (1, .left, 14)],
+  [some (1, .right, 3), some (1, .right, 15)],
+  [some (0, .right, 0), some (0, .left, 17)],
+  [some (0, .right, 1), some (1, .left, 17)],
+  [some (1, .left, 19), some (1, .left, 18)],
+  [some (0, .left, 20), some (0, .left, 8)],
+  [some (0, .right, 1), some (0, .left, 20)]
+]
+
+/-- The 21-state Goldbach machine. -/
+def goldbach21 : Machine 21 2 := Machine.ofRows goldbach21Rows
+
+end Machines
+
+/-- The configuration `n` steps in from `init`, or `none` once `M` has halted. -/
+def run (M : Machine states symbols) (n : ℕ) : Option (Cfg states symbols) :=
+  (fun c => c.bind (step M))^[n] (some init)
+
+/-- `M`, started in state `0` on the all-blank tape, has not halted within `n` steps. -/
+def Runs (M : Machine states symbols) (n : ℕ) : Prop := (run M n).isSome
+
+instance (M : Machine states symbols) (n : ℕ) : Decidable (Runs M n) :=
+  inferInstanceAs (Decidable ((run M n).isSome = true))
+
+end ConjectureMachines

LeanPool/CryptidsGoldbach/Propositions.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Google LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maxence Faldor, Moritz Firsching
+-/
+module
+
+public import Mathlib.Data.Nat.Prime.Basic
+
+/-!
+# Goldbach's conjecture
+
+The arithmetic proposition used by the Goldbach machine semantics.
+-/
+
+@[expose] public section
+
+namespace ConjectureMachines
+
+/-- Every even natural number greater than two is the sum of two primes. -/
+def GoldbachConjecture : Prop :=
+  ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q
+
+end ConjectureMachines

LeanPool/CryptidsGoldbach/Semantics.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Google LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maxence Faldor, Moritz Firsching
+-/
+module
+
+public import LeanPool.CryptidsGoldbach.Goldbach21
+public import LeanPool.CryptidsGoldbach.Propositions
+
+/-!
+# Semantics of the Goldbach Turing Machines (`goldbach_25` and `goldbach_21`)
+
+This file proves that the 25-state baseline Turing machine `reference` (`goldbach_25`) and the
+21-state compressed Turing machine `candidate` (`goldbach_21`) halt on the blank tape if and only
+if Goldbach's conjecture is false (i.e., there exists an even integer $n > 2$ that cannot be
+written as the sum of two primes).
+
+## Provenance and Attribution
+
+* **Original 27-state (26-state reachable) Goldbach Turing machine (2016)**:
+  Published anonymously in a GitHub Gist
+  (<https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6>) and popularized by
+  Scott Aaronson and the Busy Beaver Challenge community
+  (<https://wiki.bbchallenge.org/wiki/Cryptids>).
+* **25-state optimization and first Lean 4 verification (2024)**:
+  Yijun Leng optimized the machine from 26 reachable states to 25 states (`goldbach_25`, the
+  `reference` machine here) and formalized its correctness in Lean 4 in
+  <https://github.com/lengyijun/goldbach_tm> (released under the Apache-2.0 license).
+* **21-state compression and halting-equivalence proof (2026)**:
+  Maxence Faldor and Moritz Firsching (using Gemini Argon) found the 21-state machine `candidate`
+  (`goldbach_21`) and proved `Halts reference ↔ ∃ w : ℕ, ¬ HasGoldbachPair (2 * w + 4)` and
+  `Halts candidate ↔ Halts reference` in `Cryptids.Goldbach21`.
+-/
+
+@[expose] public section
+
+namespace ConjectureMachines.Goldbach21.Semantics
+
+open Turing StateTransition
+open ConjectureMachines.Goldbach21
+
+/-- Equivalence between `IsPrime` in `Cryptids.Goldbach21` and Mathlib's `Nat.Prime`. -/
+theorem isPrime_iff_prime (n : ℕ) : IsPrime n ↔ Nat.Prime n :=
+  Nat.prime_def_lt'.symm
+
+/-- Equivalence between `HasGoldbachPair (2 * w + 4)` for all `w` and `GoldbachConjecture`. -/
+theorem goldbachConjecture_iff_all_stages :
+    GoldbachConjecture ↔ ∀ w : ℕ, HasGoldbachPair (2 * w + 4) := by
+  constructor
+  · intro hG w
+    obtain ⟨p, q, hp, hq, hn⟩ := hG (2 * w + 4) (by omega) ⟨w + 2, by omega⟩
+    exact ⟨p, q, (isPrime_iff_prime p).mpr hp, (isPrime_iff_prime q).mpr hq, hn.symm⟩
+  · intro hall n hn2 ⟨k, hk⟩
+    have hk2 : 2 ≤ k := by omega
+    obtain ⟨a, b, ha, hb, hab⟩ := hall (k - 2)
+    exact ⟨a, b, (isPrime_iff_prime a).mp ha, (isPrime_iff_prime b).mp hb, by omega⟩
+
+/-- The 25-state baseline machine `reference` (`goldbach_25`) halts on the blank tape
+if and only if Goldbach's conjecture is false. -/
+theorem halts_reference_iff_not_goldbach :
+    Halts reference ↔ ¬ GoldbachConjecture := by
+  change Halts refM ↔ ¬ GoldbachConjecture
+  rw [halts_reference_iff_exists_counterexample, goldbachConjecture_iff_all_stages]
+  push Not
+  rfl
+
+/-- The 21-state machine `candidate` (`goldbach_21`) halts on the blank tape
+if and only if Goldbach's conjecture is false. -/
+theorem halts_candidate_iff_not_goldbach :
+    Halts candidate ↔ ¬ GoldbachConjecture :=
+  candidate_equivalent.trans halts_reference_iff_not_goldbach
+
+end ConjectureMachines.Goldbach21.Semantics

LeanPool/projects/cryptids-goldbach.yaml

@@ -0,0 +1,43 @@
+slug: cryptids-goldbach
+title: A 21-state Turing machine for Goldbach's conjecture
+summary: A concrete 21-state binary Turing machine halts on the blank tape exactly when
+  Goldbach's conjecture is false. The proof connects it to the earlier 25-state machine,
+  verifies both machines' prime-search semantics, and preserves finite-machine execution,
+  tape-scanning and reachability infrastructure. This imports only the Goldbach dependency
+  closure of Cryptids, excluding its Riemann, ZF and Busy Beaver developments.
+branch: computability and number theory
+entry_module: LeanPool.CryptidsGoldbach
+authors:
+- Maxence Faldor
+- Moritz Firsching
+source:
+  url: https://github.com/google-deepmind/cryptids/tree/f873434871b2301d5c8c91ba6fa224f92c93c1e1
+  github_repo: google-deepmind/cryptids
+  commit: f873434871b2301d5c8c91ba6fa224f92c93c1e1
+  announcement_url: https://leanprover.zulipchat.com/#narrow/channel/579630-Project-announcements/topic/Cryptids/near/632199475
+  announcement_date: '2026-10-16'
+license: Apache-2.0
+status: verified
+provenance: AI
+main_declarations:
+- ConjectureMachines.Goldbach21.Semantics.halts_candidate_iff_not_goldbach
+main_results:
+- declaration: ConjectureMachines.Goldbach21.Semantics.halts_candidate_iff_not_goldbach
+  informal: The explicit 21-state binary Turing machine halts from the blank tape if and
+    only if some even natural number greater than two is not the sum of two primes.
+- declaration: ConjectureMachines.Goldbach21.candidate_equivalent
+  informal: The explicit 21-state and 25-state binary machines have the same blank-tape
+    halting behavior.
+- declaration: ConjectureMachines.Goldbach21.candidate_fewer_states
+  informal: The candidate machine has 21 states, strictly fewer than the reference's 25.
+- declaration: ConjectureMachines.Goldbach21.Semantics.halts_reference_iff_not_goldbach
+  informal: The 25-state reference machine halts from the blank tape exactly when
+    Goldbach's conjecture is false.
+tags:
+- computability
+- turing-machines
+- goldbach-conjecture
+- machine-simulation
+msc:
+- 03D10
+- 11P32