DeepMind uses Gemini Argon to shrink Turing machines for three math problems
Google DeepMind used Gemini Argon to reduce Turing machine state counts for Goldbach's Conjecture, the Riemann Hypothesis and ZF consistency, verifying each reduction end-to-end in Lean 4 and open-sourcing the code.
It has been a blast hunting cryptids with such a great team 👾 Alongside the Busy Beaver holdout proofs, we also open-sourced smaller 2-symbol Turing machines for three foundational math problems, verified end-to-end in Lean 4 from a blank tape to Mathlib (0 sorry): - Goldbach's Conjecture: 25 -> 21 states - Riemann Hypothesis: 120 -> 104 states - ZF Consistency: 393 -> 380 states Using Gemini Argon, we compressed the community baseline machines and proved both the state reductions and full mathematical semantics in the kernel: each machine halts if and only if the conjecture fails (or ZF is inconsistent). Best part of releasing this openly: within days of going live, a community contributor already built on our 104-state proof to push the Riemann machine down to 95 states. 🚀 Huge thanks to everyone across the @GoogleDeepMind team who contributed to this project: @tomzahavy, @robertarail, @dsantosmarco, @vivek_veeriah, @Dahoas1, @zuza777, @MoritzFirsching, Andrew Bolt, Satinder Singh, Hussain Masoom, and Petar Sirkovic, as well as the Busy Beaver community. Code: https://github.com/google-deepmind/cryptids
This post quotes another post: “DeepMind uses Gemini 4 Argon to find 20 new Busy Beaver cryptids”