02 Alphabet (Google / Google DeepMind)

1. Company and research division. Google DeepMind (with University of Cambridge affiliation for the lead author); secondary item: Google Research Coral NPU (edge hardware IP) in Synaptics Astra SR200.

2. Date of publication / announcement. arXiv:2610.22603. v1 submitted 15 October 2026 and announced 19 October; v2 dated 20 October 2026. The submission dates come from an arXiv mirror/listing; the abstract page itself showed no date. Coral NPU/SR200: Synaptics press release, 20 October 2026.

3. Research title and field. 'At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier'. Field: AI for mathematics, automated conjecturing, formal verification (Lean 4).

4. Research background. BB(n) is the maximum number of steps a halting n-state, 2-symbol Turing machine can run from a blank tape. It is uncomputable and grows faster than any computable function. The community determined BB(5) = 47,176,870 without AI (STOC 2026). BB(6) still has about 1,094 'holdout' machines whose halting status is unknown. Some of them, called Cryptids, reduce to open Collatz-like problems.

5. Scientific innovation. An autonomous pipeline that discovers structure rather than solving a human-posed problem. It treats Turing machines as grey boxes, conjectures compact macro-transition rules from simulation data, and proves the rules in Lean 4 using a multi-persona agent (Problem Setter, Planner, Writer, Critic). The agent may revise the formal statements it was seeded with, but not the machine definition or the start configuration.

6. Methodology. Every stage uses Gemini 3.1 Pro; a second stage used an auto-research system with Gemini 3.8 Flash. The process runs as follows:

• Pattern detection: each machine is simulated for S = 5×10^6 steps; tapes are compressed into run-length blocks with a simplicity score, and the top K = 100 patterns are kept.
• Conjecturing: Python transition functions are written and refined over up to N = 5 turns, using an interactive simulator capped at 128,000 steps per synthetic transition.
• Filtering: only conjectures with 100% empirical accuracy pass.
• Informal proving: a generator–evaluator loop with up to M = 4 iterations scores correctness and format.
• Formal proving: Lean 4.28.1 with BusyLean, a 72-hour cap, and acceptance only with no sorry and no unauthorised axioms.

The search covered 1,094 BB(6) holdouts, 65 BB(2,5) holdouts and 4 BB(3,3) holdouts. The authors manually validated the final Lean statements.

7. Results. 52 candidate machines were found (50 in BB(6)). Formally verified Collatz-like accelerations were obtained for 11 BB(6) machines with no prior documented analysis; the authors provisionally classify these as 'Cryptids'. Formal proofs or higher-level accelerations were also obtained for 15 previously studied machines (14 BB(6) and 1 BB(2,5)). Lean proofs and code are public (github.com/google-deepmind/cryptids).

8. Scientific significance. This is one of the cleaner demonstrations of AI-driven mathematical discovery with machine-checked guarantees. Results can be checked independently by compiling the Lean code, which reduces reliance on trust in the model.

9. Technical limitations. The work is a preprint and has not been peer-reviewed. Cryptid status is 'subject to community acceptance', and the paper's definition is broader than the community's. The approach targets only Collatz-like dynamics and does not resolve halting. Some rediscoveries were proved but not checked by hand. Compute cost is not reported.

10. Technology readiness and evidence type. Method: lab prototype. Evidence: preprint, with formally verified (machine-checked) outputs. Not yet independently reproduced by the bbchallenge community.

11. Competitive comparison. Comparable work: AlphaEvolve (search over code with a reward signal), LEAP and AI Co-Mathematician (assistive), and community use of Claude Opus 4.6 for FRACTRAN BB_f non-halting proofs (cited by the authors). This work is distinctive for combining autonomous conjecturing with end-to-end Lean verification.

12. Future research (1–5 years) — FORECAST. FORECAST (1–5 years): extension beyond Collatz-like dynamics; community adjudication of the 11 machines; similar 'observe–conjecture–formalise' pipelines applied to combinatorics and dynamical systems; Lean-verified AI contributions becoming routine in open-problem catalogues.

13. Original references.

• https://arxiv.org/abs/2610.22603
• https://github.com/google-deepmind/cryptids
• https://investor.synaptics.com/news-releases/news-release-details/synaptics-launches-xmcutm-era-astrar-sr200-series-multimodal
• https://www.nature.com/articles/s41591-026-04626-w