Google DeepMind's Gemini agent finds Lean-verified rules for eleven BB(6) machines

Google DeepMind published a paper saying a Gemini-based agent found and formally verified new acceleration rules for eleven unresolved Turing machines in BB(6), the current frontier of the Busy Beaver problem.

The rules are kept only after a Lean proof, so the authors say the result does not depend on trusting the model's reasoning. Each rule first goes through informal reasoning before the proof. The authors provisionally call these machines Cryptids, and their halting behavior remains unresolved.