Google DeepMind Team Uses Lean to Verify 11 Busy Beaver Descriptions

Researchers at Google DeepMind and the University of Cambridge used an AI system to formalize the behavior of 11 six-state Turing machines in the BB(6) set. The work provides a compact description of each machine’s behavior, but does not resolve whether any of the 11 eventually stops.

The descriptions cover runs that begin with a blank tape. They condense behavior that might otherwise take many steps to trace into rules that can be checked by a computer. Lean 4 checked formal proofs of those rules. Verifying a machine’s described behavior does not establish whether it ultimately halts or continues indefinitely.

The system, Gemini 3.1 Pro, combined simulations with pattern detection and AI-generated conjectures. Researchers used those elements to develop the rules and then checked their proofs with Lean 4, a theorem prover. The result is a machine-checkable account of the runs, while the halt-or-continue question remains open.

The machines are part of the Busy Beaver problem. For a fixed number of states and two symbols, the problem asks which machine runs the longest among those that eventually halt. No general procedure can calculate the Busy Beaver value for every possible number of states. Machines with unresolved halting status are known as holdouts.

The initial search examined 1,094 BB(6) holdouts, along with 65 machines in BB(2,5) and four in BB(3,3). It produced 52 candidates across those three sets, 50 of them in BB(6). Further analysis of the candidates yielded the 11 results in the study. The 52-candidate total covers all three sets, rather than only the 1,094 BB(6) holdouts.

The researchers provisionally call the 11 machines “Cryptids.” The label refers to machines with concise mathematical descriptions but unresolved halting status, and it still awaits acceptance by the Busy Beaver community.