Researchers from Google DeepMind and the University of Cambridge have developed an AI system based on Gemini that identifies and proves mathematical patterns in Turing machines. The project focuses on the Busy Beaver problem, specifically analyzing machines with six states and two symbols.
The AI agent operates by identifying repetitive structures in simulation results, formulating hypotheses, and creating mathematical rules. These rules are then formally verified using the Lean 4 environment, which ensures the accuracy of the mathematical reasoning.
The system successfully derived and verified new rules for 11 previously unanalyzed machines in the BB(6) class. These rules allow for the description of multiple computation steps simultaneously, mirroring structures found in the Collatz conjecture.
In addition to the 11 new cases, the team obtained formal proofs or new analysis methods for 15 machines that had been previously studied by the mathematical community. The researchers noted that while these rules describe machine behavior, they do not yet determine if the machines halt.
The authors propose classifying these instances as Cryptids, representing machines with compact mathematical descriptions but unknown halting status. Future research will explore whether this method can be extended to other types of computational behavior beyond Collatz-like patterns.
