DeepMind's Gemini agent proved rules for 11 Busy Beaver machines, not whether they halt

A team at Google DeepMind has used an agent built on Gemini to analyse Turing machines on the Busy Beaver frontier, and it produced formally verified rules for 11 six-state machines that no one had documented before, according to a paper posted to arXiv on October 15. The catch is in the result itself: the rules show these machines behave like Collatz-style number puzzles, so whether they ever stop remains unknown.

The authors provisionally call the 11 machines "Cryptids," subject to acceptance by the Busy Beaver community.

Why the Busy Beaver frontier is hard

The Busy Beaver problem asks how many steps the longest-running halting machine of a given size can take. The value is uncomputable in general, and the fifth Busy Beaver number was settled only recently through a collaborative community proof that, the paper notes, used no AI.

Settling the next value, BB(6), means classifying every six-state machine as halting or running forever. The ones left over after automated filters are called holdouts. Some of them turn out to encode open mathematical questions, and those are the Cryptids.

What the agent actually did

The pipeline simulates a machine, looks for repeating patterns on its tape, and has Gemini 3.1 Pro conjecture an "acceleration": a compact rule that jumps many steps ahead in one go. Rules must predict the simulated data with 100% accuracy before Gemini attempts an informal proof, and an agent then writes a formal proof in the Lean 4 theorem prover.

The team ran it over 1,094 BB(6) holdouts compiled by the community member mxdys, plus 65 holdouts from a related set and 4 from another. The broad search flagged 52 promising machines, 50 of them six-state machines.

From those, the system produced new, proven accelerations for 11 machines with no prior documented analysis. It also gave formal proofs or higher-level rules for 15 machines whose behaviour community members had already described, often in Discord messages, but had not verified. The authors say they checked the final Lean statements by hand, and the proofs are public.

What it did not do

None of this decides whether the 11 machines halt. Each now reduces to a Collatz-like question, the same family as the famous conjecture that has resisted mathematicians for decades.

The authors are frank about the limits. They write that the approach is "not entirely open-ended," because it only looks for Collatz-like structure that mathematicians already study, and that any insight into the Collatz conjecture itself "remain speculative."

The next step they describe is a system that could discover new kinds of open problems hidden inside Turing machines, not just recognise a familiar one.