A Gemini-based system found and formally verified compact rules for 11 previously unanalyzed six-state Turing machines
An AI agent built by Google DeepMind and University of Cambridge researchers has done something math competitions never ask for. It wandered into an unsolved corner of computer science and came back with new, verified results.
The Gemini-based agentic system discovered compact mathematical acceleration rules for 11 previously unanalyzed six-state Turing machines . It then proved those rules formally, in a format any skeptic can check line by line.
The work is documented in a preprint posted to arXiv on October 15, 2026, under the identifier 2610.22603. The research team includes Google DeepMind researchers Marco Dos Santos, Tom Zahavy, and Vivek Veeriah, working with ties to the University of Cambridge.
The target was the Busy Beaver BB(6) frontier. This is a collection of six-state Turing machines whose long-term behavior nobody has managed to pin down.
The central question for each machine is deceptively simple: does it eventually stop, or does it run forever? The Busy Beaver problem is famous for being uncomputable, meaning no general algorithm can answer that question for every machine.
The DeepMind system examined 1,094 of these BB(6) holdouts. From that pool, the agent flagged 52 machines as worth deeper study. It ultimately confirmed new verified results for 11 machines that had not been analyzed before.
The results take the form of acceleration rules. Rather than simulating a machine one painstaking step at a time, an acceleration rule describes its behavior compactly.
The researchers have provisionally labeled these 11 machines “Cryptids.”
Daily. Free. Join 34,000+ readers across crypto, finance, and policy.
The new rules describe how the machines behave. They do not, however, conclusively settle whether the machines ever halt.
The pipeline combines three activities: the system runs simulations, generates conjectures from what it observes, and then constructs formal proofs.
Those proofs are written in Lean 4, a theorem prover. If a single logical step is missing, it rejects the proof outright.
Gemini served as the engine generating the formal proofs for all 11 newly verified BB(6) machines. Because the output runs through Lean, correctness does not depend on trusting the model.
The proof artifacts have been released publicly. Community follow-ups were reported within days of publication.
The DeepMind and Cambridge paper pitches the Busy Beaver problem as an experimental ground for open-ended mathematical discovery, marking a deliberate departure from traditional competitive problem-solving formats.
The Busy Beaver frontier also offers a useful property for this kind of experiment. Each machine is small and precisely defined, so progress is easy to measure. Either a verified rule exists for a machine, or it does not.
The funnel from 1,094 holdouts to 52 flagged machines to 11 verified results tells a realistic story about the research process. Most leads did not pan out.
The Cryptids remain unresolved on the halting question, and the work describes behavior rather than delivering final verdicts.