Researchers from Google DeepMind and the University of Cambridge utilized an agentic system powered by Gemini to analyze the Busy Beaver BB(6) problem. The team examined 1,094 six-state Turing machines, identifying 52 candidates for further investigation.
The system successfully generated and formally verified compact acceleration rules for 11 previously unanalyzed machines. These rules describe machine behavior without requiring step-by-step simulation, though they do not determine if the machines eventually halt.
The research process involved running simulations, generating conjectures, and constructing proofs in the Lean 4 theorem prover. This approach ensures that the results are logically sound and independent of the model's reliability.
The findings were documented in a preprint published on arXiv on October 15, 2026, under identifier 2610.22603. The research team includes Marco Dos Santos, Tom Zahavy, and Vivek Veeriah.
