Certified State Reductions and Semantics of Conjecture-Checking Turing Machines

Google DeepMind researchers Maxence Faldor and Moritz Firsching published a repository of formally verified 2-symbol Turing machines with Lean 4 semantics proofs for Goldbach's Conjecture, ZF Set Theory Consistency, and the Riemann Hypothesis, including a 21-state Goldbach machine reduced from a 25-state machine and a 104-state Riemann machine reduced from a 120-state machine. The proofs are checked by the Lean 4 kernel v4.35.0-rc4 without sorry and use only the standard axioms propext, Classical.choice, and Quot.sound. Each reduced machine halts from the blank tape if and only if its reference machine halts, and the semantics proofs establish conditions such as Halts candidate ↔ ¬ GoldbachConjecture and ¬ RiemannHypothesis.

This repository contains formally verified 2-symbol Turing machines and Lean 4 semantics proofs for Goldbach's Conjecture , ZF Set Theory Consistency , and the Riemann Hypothesis , developed by Maxence Faldor and Moritz Firsching using Gemini Argon. | Conjecture | Machine | States | Source / Provenance | Proved Halting Condition Halts M ↔ ... | Lean 4 Proofs | |---|---|---|---|---|---| | Goldbach's Conjecture | goldbach 21 | 21 | Reduced from goldbach 25 25 states, Yao / Leng 2024 | ¬ GoldbachConjecture | Goldbach21.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Goldbach21.lean , Semantics/Goldbach.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/Goldbach.lean | | ZF Consistency | zf 380 | 380 | Reduced from zf 393 393 states, Wade Aug 2026 | ZFInconsistent ¬ Halts candidate proved | Zf380.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Zf380.lean , Semantics/Zf393.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/Zf393.lean | | ZF Consistency | zf 393 | 393 | Andrew Wade turing machine explorer https://codeberg.org/ajwade/turing machine explorer 9c5c2e82 , Aug 2026 | ZFInconsistent ¬ Halts zf393 proved | Zf393.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Zf393.lean , Semantics/Zf393.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/Zf393.lean | | ZF Consistency | zf 432 | 432 | Andrew Wade turing machine explorer https://codeberg.org/ajwade/turing machine explorer 33b30300 , Aug 2025 | WadeZFInconsistent | Semantics/Zf.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/Zf.lean | | Riemann Hypothesis | riemann 104 | 104 | Reduced from riemann 120 120 states, Shunia Sept 2026 | ¬ RiemannHypothesis | Riemann104.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Riemann104.lean , Semantics/Riemann120.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/Riemann120.lean | | Riemann Hypothesis | riemann 120 | 120 | Joseph M. Shunia arXiv:2609.30306 https://arxiv.org/abs/2609.30306 , Sept 2026 | ¬ RiemannHypothesis | Riemann120.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Riemann120.lean , Semantics/Riemann120.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/Riemann120.lean | | Riemann Hypothesis | riemann 744 | 744 | Matiyasevich, O'Rear & Aaronson riemann 744 sorear.tm , 2016 | ¬ RiemannHypothesis | Semantics/Riemann.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/Riemann.lean | See RELATED WORK.md https://github.com/google-deepmind/cryptids/blob/main/RELATED WORK.md for the historical progression across each domain. All proofs in Cryptids/ https://github.com/google-deepmind/cryptids/blob/main/Cryptids are checked by the Lean 4 kernel v4.35.0-rc4 without sorry and use only the standard axioms propext , Classical.choice , Quot.sound : 1. State reduction and halting equivalence candidate.states < reference.states and Halts candidate ↔ Halts reference : Each reduced record machine goldbach 21 , zf 380 , riemann 104 has fewer states than its reference machine goldbach 25 , zf 393 , riemann 120 and halts from the blank tape if and only if the reference machine halts Goldbach21.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Goldbach21.lean , Zf380.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Zf380.lean , Riemann104.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Riemann104.lean . 2. End-to-end mathematical semantics Cryptids/Semantics/ https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/README.md : - Goldbach goldbach 21 and goldbach 25 : Both goldbach 21 and goldbach 25 halt if and only if Goldbach's conjecture is false Halts candidate ↔ ¬ GoldbachConjecture . - Riemann Hypothesis riemann 104 , riemann 120 , and riemann 744 : All three machines riemann 104 , Shunia's 120-state machine riemann 120 , and the 744-state machine riemann 744 halt if and only if Mathlib's RiemannHypothesis is false Halts candidate ↔ ¬ RiemannHypothesis , Halts riemann120 ↔ ¬ RiemannHypothesis , and Halts riemann744 ↔ ¬ RiemannHypothesis . - ZF Consistency zf 380 , zf 393 , and zf 432 : Both zf 380 and Wade's 393-state machine zf 393 incorporating upstream fix 10fcf152b3 halt if and only if O'Rear's zf2.nql Hilbert system proves$v 0 \in v 0$ Halts candidate ↔ ZFInconsistent , Halts zf393 ↔ ZFInconsistent , and hence never halt in ZFSet.{0} not halts candidate , not halts zf393 , while zf 432 halts if and only if the 20-clause deductive system enumerated by zf 432 wade.tm derives$v 0 \in v 0$ WadeZFInconsistent . 3. Details on the proof architecture and mathematical background are in Cryptids/Semantics/README.md https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/README.md . For the reduced machines in artifacts/ https://github.com/google-deepmind/cryptids/blob/main/artifacts , the state-space transformations affect execution step counts as follows: - goldbach 21 339,411 vs. 170,966 steps through n = 40 , 1.99x : Eliminating 4 states 1, 8, 10, 17 reverses the partition enumeration to test larger summands first and routes divisor acceptance through the main counter-tape scanner. - zf 380 +0.093% step overhead at 1,000,000 steps; 0 step overhead during 39,753 -step bootstrap : Eliminating 13 states 65, 68, 266, 278, 322, 335, 341, 353, 359, 361, 379, 387, 389 via a 5-cell sliding-window invariant validState and non-destructive leftward head bounces 1, 3, 5, 7, 9 steps preserves 100% bit-exact tape equality after every macro-step. - riemann 104 9,037 vs. 89,775,610 bootstrap steps, 9,934.23x faster initialization; 498,382 vs. 111,294,346 total steps over the first 1,000 register instructions, 223.31x speedup : Eliminating 16 states 120 - 104 splits merged scanner state 32 via a 5-cell window invariant 120 - 121 , replaces the two-phase 89.8M -step bootstrap -9 states with a self-bootstrapping header and dynamic on-demand zero padding padTotal - padTotal + 1 , and consolidates return scanners and binary call-stack frames mapStack , -8 states . Build all Lean 4 proofs: lake exe cache get lake build Independently audit the proofs against Challenge.lean https://github.com/google-deepmind/cryptids/blob/main/Challenge.lean with leanprover/comparator https://github.com/google-deepmind/cryptids/blob/main/comparator/README.md : lake comparator --config comparator/all.json Run the standalone zero-dependency Python verifier re-compiles upstream baseline sources, checks SHA-256 digests and transition tables, and simulates 250,000 steps per domain : python3 verify.py - Cryptids/ https://github.com/google-deepmind/cryptids/blob/main/Cryptids — Shared problem definitions Propositions.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Propositions.lean , Turing machine specifications Machines.lean https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Machines.lean , halting-equivalence proofs, and end-to-end semantics Cryptids/Semantics/README.md https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/README.md . - Challenge.lean https://github.com/google-deepmind/cryptids/blob/main/Challenge.lean & comparator/ https://github.com/google-deepmind/cryptids/blob/main/comparator — Self-contained target theorem specification and configuration files for leanprover/comparator https://github.com/google-deepmind/cryptids/blob/main/comparator/README.md . - artifacts/ https://github.com/google-deepmind/cryptids/blob/main/artifacts — Canonical machine.txt transition tables and reduction write-ups for goldbach 21 https://github.com/google-deepmind/cryptids/blob/main/artifacts/goldbach 21/README.md , zf 380 https://github.com/google-deepmind/cryptids/blob/main/artifacts/zf 380/README.md , and riemann 104 https://github.com/google-deepmind/cryptids/blob/main/artifacts/riemann 104/README.md . - baselines/ https://github.com/google-deepmind/cryptids/blob/main/baselines — Verbatim upstream source files, canonical 5-tuple tables, and PROVENANCE.md https://github.com/google-deepmind/cryptids/blob/main/baselines/PROVENANCE.md . - RELATED WORK.md https://github.com/google-deepmind/cryptids/blob/main/RELATED WORK.md — Literature lineage and Q, 2 Turing machine conventions. - verify.py https://github.com/google-deepmind/cryptids/blob/main/verify.py — Standalone Python 3 verification script. Pull requests and issues are welcome, especially for smaller Turing machines for these problems, machines for other conjectures, or streamlined Lean proofs. Please also open an issue if you notice anything amiss, such as a missing reference or provenance detail. See CONTRIBUTING.md https://github.com/google-deepmind/cryptids/blob/main/CONTRIBUTING.md for general guidelines. We thank Eric Wieser for careful review, as well as the Busy Beaver Challenge community, Yijun Leng, Stefan O'Rear, Yuri Matiyasevich, Scott Aaronson, Adam Yedidia, Andrew Wade, and Joseph Shunia for the baseline Turing machines and compilers, and the Mathlib community. Copyright 2026 Google LLC All software is licensed under the Apache License, Version 2.0 Apache 2.0 ; you may not use this file except in compliance with the Apache 2.0 license. You may obtain a copy of the Apache 2.0 license at: https://www.apache.org/licenses/LICENSE-2.0 https://www.apache.org/licenses/LICENSE-2.0 All other materials are licensed under the Creative Commons Attribution 4.0 International License CC-BY . You may obtain a copy of the CC-BY license at: https://creativecommons.org/licenses/by/4.0/legalcode https://creativecommons.org/licenses/by/4.0/legalcode Unless required by applicable law or agreed to in writing, all software and materials distributed here under the Apache 2.0 or CC-BY licenses are distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the licenses for the specific language governing permissions and limitations under those licenses. This is not an official Google product.