Gemini Agent Formally Verifies New Busy Beaver Math Results
The workflow itself is the lesson: an agent chose its own research targets, then gated every output through Lean verification, a pattern that transfers to other open math and code-verification domains. Researchers and agent builders can replicate the propose-then-verify loop without trusting model outputs. Compared with earlier autoformalization work, this one attacks uncomputable problems where no fixed benchmark list exists.
Google DeepMind published a paper on open-ended mathematical discovery using a Gemini-based agent. The agent selected eleven unresolved Turing machines in BB(6), the current frontier of the Busy Beaver problem, and proposed acceleration rules for them. Each rule passed through informal reasoning and a formal Lean proof before being kept, so results do not rely on trusting the model. The eleven machines, provisionally named Cryptids, now have exact compact execution descriptions, though whether they halt remains open. The paper is available at arxiv.org/abs/2610.22603.
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-the-… 💬 13 🔄 2 ❤️ 28 👀 2016 📊 15 ⚡
