---
id: "2026-10-09-deepmind-cryptids-smaller-turing-machines-goldbach-riemann-zf"
url: "https://postcutoff.com/e/2026-10-09-deepmind-cryptids-smaller-turing-machines-goldbach-riemann-zf/"
as_of: "2026-10-17T02:25:00+02:00"
date: "2026-10-09"
date_precision: day
category: science
importance: 3
confidence: high
status: [Result confirmed]
verification: Lean-verified
sources: 3
editor: human editor
human_review: null
version: "2026-10-16"
---

As of: 2026-10-17 02:25 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-09-deepmind-cryptids-smaller-turing-machines-goldbach-riemann-zf/

# Gemini Argon shrinks Goldbach, Riemann and ZF Turing machines

Full title: DeepMind researchers use Gemini Argon to shrink the record Turing machines that encode Goldbach (25→21 states), the Riemann Hypothesis (120→104) and ZF consistency (393→380), with Lean proofs

A Google DeepMind GitHub repo ("cryptids", created Oct 9, 2026) by Maxence Faldor and Moritz Firsching, "using Gemini Argon", gives smaller 2-symbol Turing machines whose halting is equivalent to a counterexample to Goldbach's conjecture (21 states, from 25), to the falsity of the Riemann Hypothesis (104, from 120) and to an inconsistency of ZF (380, from 393). Each reduction is proved in Lean 4 to halt exactly when the previous record machine does, without sorry, and audited with leanprover/comparator.

## Key facts
- Goldbach: goldbach_21 reduces the 25-state machine (Yao / Leng 2024) by removing 4 states; Lean proof that Halts M ↔ ¬GoldbachConjecture
- Riemann Hypothesis: riemann_104 reduces Joseph Shunia's 120-state machine (Sept 2026, arXiv 2609.30306), itself down from O'Rear's 744 states (2016); Halts M ↔ ¬RiemannHypothesis using Mathlib's definition
- ZF: zf_380 reduces Andrew Wade's 393-state machine (Aug 2026), down from 432 (2025); its halting is equivalent to O'Rear's Hilbert system deriving a contradiction, and the repo proves it never halts in ZFSet
- The repo also has kernel-checked behaviour proofs for some BB(6) holdout machines (potential 'Cryptids', subject to community acceptance)
- All proofs checked by the Lean kernel without sorry, using only the standard axioms; reviewed by Eric Wieser; Lean v4.35.0-rc4
- AI role, as stated in the repo: the machines and Lean semantics were 'developed by Maxence Faldor and Moritz Firsching using Gemini Argon'; no paper or blog post yet
- Context: Yedidia and Aaronson (2016) started this line of work, which bounds where the Busy Beaver function becomes independent of ZF; records are tracked on the bbchallenge wiki

## What happened

The repo appeared quietly on DeepMind's GitHub on Oct 9 and was found by our sweep's watched-accounts step on Oct 16 (44 stars). It
is a formal-verification package, not an announcement: the AI role is one line in the library README and in the history table, which
credits each new record to "Faldor & Firsching, using Gemini Argon".

## Why it matters

Smaller machines tighten the known bounds on where the Busy Beaver function stops being computable from standard mathematics. Each
reduction comes with machine-checked proofs, so the new records can be checked without trusting the model or the authors. It is also
one of the first Gemini 4 Argon research results we have seen.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 162 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 101 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 192 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 131 days after its cutoff

## Sources

1. [GitHub: google-deepmind/cryptids (Some Cryptids and Lean proofs)](https://github.com/google-deepmind/cryptids) (github.com, code)
2. [cryptids: Cryptids/README.md (records table and provenance)](https://github.com/google-deepmind/cryptids/blob/main/Cryptids/README.md) (github.com, code)
3. [bbchallenge wiki: Cryptids](https://wiki.bbchallenge.org/wiki/Cryptids) (wiki.bbchallenge.org, discussion)

## Changes

- 2026-10-16 (filed): Created (read the README, library README, RELATED_WORK and PROVENANCE)

## Related

- 2026-10-13: [Google releases Gemini 4 Argon broadly](https://postcutoff.com/e/2026-10-13-gemini-4-argon-general-availability/index.md)
- People: [Scott Aaronson](https://postcutoff.com/person/scott-aaronson/)