Cryptids.Semantics.Goldbach

Cryptids
Semantics
Goldbach

Imports

/-
Copyright (c) 2026 Google LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
module

public import Cryptids.Goldbach21
public import Cryptids.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 sectionnamespace ConjectureMachines.Goldbach21.Semanticsopen Turing StateTransitionopen 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⊢ GoldbachConjecture ↔ ∀ (w : ℕ), HasGoldbachPair (2 * w + 4)
  constructormp⊢ GoldbachConjecture → ∀ (w : ℕ), HasGoldbachPair (2 * w + 4)mpr⊢ (∀ (w : ℕ), HasGoldbachPair (2 * w + 4)) → GoldbachConjecture
  ·mp⊢ GoldbachConjecture → ∀ (w : ℕ), HasGoldbachPair (2 * w + 4) intro hG wmphG:GoldbachConjecturew:ℕ⊢ HasGoldbachPair (2 * w + 4)
    obtain ⟨p, q, hp, hq, hn⟩ := hG (2 * w + 4) (byhG:GoldbachConjecturew:ℕ⊢ 2 < 2 * w + 4 omegaAll goals completed! 🐙) ⟨w + 2, byhG:GoldbachConjecturew:ℕ⊢ 2 * w + 4 = w + 2 + (w + 2) omegaAll goals completed! 🐙⟩mphG:GoldbachConjecturew:ℕp:ℕq:ℕhp:Nat.Prime phq:Nat.Prime qhn:2 * w + 4 = p + q⊢ HasGoldbachPair (2 * w + 4)
    exact ⟨p, q, (isPrime_iff_prime p).mpr hp, (isPrime_iff_prime q).mpr hq, hn.symm⟩All goals completed! 🐙
  ·mpr⊢ (∀ (w : ℕ), HasGoldbachPair (2 * w + 4)) → GoldbachConjecture intro hall n hn2 ⟨k, hk⟩mprhall:∀ (w : ℕ), HasGoldbachPair (2 * w + 4)n:ℕhn2:2 < nk:ℕhk:n = k + k⊢ ∃ p q, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q
    have hk2 : 2 ≤ k := by⊢ GoldbachConjecture ↔ ∀ (w : ℕ), HasGoldbachPair (2 * w + 4) omegamprhall:∀ (w : ℕ), HasGoldbachPair (2 * w + 4)n:ℕhn2:2 < nk:ℕhk:n = k + khk2:2 ≤ k⊢ ∃ p q, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q
    obtain ⟨a, b, ha, hb, hab⟩ := hall (k - 2)mprhall:∀ (w : ℕ), HasGoldbachPair (2 * w + 4)n:ℕhn2:2 < nk:ℕhk:n = k + khk2:2 ≤ ka:ℕb:ℕha:IsPrime ahb:IsPrime bhab:a + b = 2 * (k - 2) + 4⊢ ∃ p q, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q
    exact ⟨a, b, (isPrime_iff_prime a).mp ha, (isPrime_iff_prime b).mp hb, byhall:∀ (w : ℕ), HasGoldbachPair (2 * w + 4)n:ℕhn2:2 < nk:ℕhk:n = k + khk2:2 ≤ ka:ℕb:ℕha:IsPrime ahb:IsPrime bhab:a + b = 2 * (k - 2) + 4⊢ n = a + b omegaAll goals completed! 🐙⟩

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⊢ reference.Halts ↔ ¬GoldbachConjecture
  change Halts refM ↔ ¬ GoldbachConjecture⊢ ConjectureMachines.Halts refM ↔ ¬GoldbachConjecture
  rw [halts_reference_iff_exists_counterexample,⊢ (∃ w, ¬HasGoldbachPair (2 * w + 4)) ↔ ¬GoldbachConjecture goldbachConjecture_iff_all_stages⊢ (∃ w, ¬HasGoldbachPair (2 * w + 4)) ↔ ¬∀ (w : ℕ), HasGoldbachPair (2 * w + 4)]⊢ (∃ w, ¬HasGoldbachPair (2 * w + 4)) ↔ ¬∀ (w : ℕ), HasGoldbachPair (2 * w + 4)
  push Not⊢ (∃ w, ¬HasGoldbachPair (2 * w + 4)) ↔ ∃ w, ¬HasGoldbachPair (2 * w + 4)
  rflAll goals completed! 🐙

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

Semantics of the Goldbach Turing Machines (goldbach_25 and goldbach_21)

Provenance and Attribution

Semantics of the Goldbach Turing Machines (`goldbach_25` and `goldbach_21`)