Researchers built a Gemini-based agent pipeline for autonomous mathematical discovery. It integrates pattern recognition, conjecturing, reasoning and formal theorem proving in Lean. The system discovered and verified new Collatz-like accelerations for eleven BB(6) Turing machines. These machines are provisionally classified as Cryptids. Cryptids admit exact compact descriptions but their halting behavior remains unresolved. The work advances analysis of BB(6) holdouts. It demonstrates potential for open-ended AI-driven mathematical discovery in computer science.