At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier

[arXiv] Marco Dos Santos, Satinder Singh, Tom Zahavy and other researchers state in a paper posted on arXiv that they have built a Gemini-based agent pipeline that integrates pattern recognition, automated conjecture generation, informal mathematical reasoning and Lean formal proofs, and use it to automatically discover "acceleration rules" for Turing machines, i.e., compact mathematical rules that summarize a large number of execution steps. The system autonomously discovered and formally verified novel Collatz-like acceleration rules for 11 machines in the "Busy Beaver" BB(6) case. The authors tentatively classify these machines as "Cryptids": their execution from a blank tape already has an exact compact mathematical description, but whether they halt remains unresolved. The authors say this classification is still awaiting community recognition.