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.

theorem ConjectureMachines.Goldbach21.Semantics.isPrime_iff_prime (n : ℕ) : IsPrime n ↔ Nat.Prime n

Equivalence between IsPrime in Cryptids.Goldbach21 and Mathlib's Nat.Prime.

theorem ConjectureMachines.Goldbach21.Semantics.goldbachConjecture_iff_all_stages : GoldbachConjecture ↔ ∀ (w : ℕ), HasGoldbachPair (2 * w + 4)

Equivalence between HasGoldbachPair (2 * w + 4) for all w and GoldbachConjecture.

theorem ConjectureMachines.Goldbach21.Semantics.halts_reference_iff_not_goldbach : reference.Halts ↔ ¬GoldbachConjecture

The 25-state baseline machine reference (goldbach_25) halts on the blank tape if and only if Goldbach's conjecture is false.

theorem ConjectureMachines.Goldbach21.Semantics.halts_candidate_iff_not_goldbach : candidate.Halts ↔ ¬GoldbachConjecture

The 21-state machine candidate (goldbach_21) halts on the blank tape if and only if Goldbach's conjecture is false.