Google DeepMind 论文：Gemini 智能体发现并形式化验证 BB(6) 中 11 台未解 Turing 机的加速规则

Banger paper from Google DeepMind on open-ended math discovery with agents.

This is one of the early, exciting works I have seen on autonomous AI-powered discoveries.

(bookmark it)

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.

Busy Beaver is uncomputable, so no fixed list of problems exists. The agent has to pick machines, spot patterns in their execution traces, and propose compact rules that summarize many steps at once.

Each proposed rule then goes through informal reasoning and a Lean proof. Only proved rules are kept, so the result does not depend on trusting the model's reasoning.

The authors provisionally call these machines Cryptids. Their runs from a blank tape now have exact, compact descriptions, but whether they halt is still open.

This is a good example of an agent producing new, formally checked mathematical results on problems it chose itself.

arxiv.org/abs/2610.22603

Chat with Paper: academy.dair.ai/papers/at-th…