Lean 4 Confirms: Gemini Agent Proved Rules for Eleven BB(6) Machines
A Gemini-based agentic system from Google DeepMind and researchers with ties to Cambridge has found and formally verified acceleration rules for eleven six-state Turing machines that no one had analyzed before. The preprint was posted to arXiv on October 15, 2026, and its correctness rests not on trust in the model but on the Lean 4 proof assistant. Yet the question that actually drives the BB(6) field — whether the machines ever halt — remains open.
The News
According to a preprint with the identifier arXiv 2610.22603, posted October 15, 2026, an agentic system built on Gemini has discovered compact mathematical acceleration rules for eleven previously unanalyzed six-state Turing machines. The system then proved the rules formally, in a format any skeptic can check line by line, as Diego Almada Lopez relates in Cryptobriefing's coverage of October 22, 2026, which draws on the preprint.
The research team includes the Google DeepMind researchers Marco Dos Santos, Tom Zahavy and Vivek Veeriah, working with ties to the University of Cambridge. The source material does not name any Cambridge co-authors or specify the exact affiliation structure, and this has not been independently confirmed beyond the preprint.
Press coverage followed on October 22, and the proof artifacts have been made publicly available. That gives the field — and everyone else — the opportunity to review what has actually been proven, rather than simply accepting a conclusion.
Why BB(6) Is a Frontier
The Busy Beaver function asks, for a given number of states, how long the longest-running Turing machine that actually halts can run before stopping. With each increase in the number of states, the difficulty explodes: the machines must be analyzed one by one, and a handful of them behave so intricately that standard methods fall short. The unanalyzed six-state machines — the "holdouts" at the BB(6) frontier — are precisely such stubborn cases.
The eleven machines this preprint concerns have been given the informal label "Cryptids": machines known to exist, but whose behavior no one has been able to properly describe. It is against this frontier that the system was aimed.
How the System Works
The funnel is concrete: the system examined 1,094 BB(6) holdouts, flagged 52 of them as worth deeper study, and ended up with new verified results for eleven machines not previously analyzed, according to Cryptobriefing's account of the preprint.
The method runs through three steps. First, simulations of the machines are run. Then conjectures are generated — compact acceleration rules describing how the machines behave over time. Finally, formal proofs of these conjectures are constructed in Lean 4, a theorem-proving program. Cryptobriefing describes the critical point this way: if a single logical step is missing, Lean rejects the proof entirely.
This is where the value lies for trust in AI-generated mathematics. A language model can err, hallucinate, or skip steps without knowing it. But a Lean proof is not an assertion — it is an artifact that is machine-checked. If the proof compiles, the theorem is proven regardless of who or what wrote it. Correctness rests on the verifier, not the model.
The Limits: Rules, Not Solutions
The most important caveat is clear, as the source relays the preprint: the new rules describe how the machines behave, but they do not settle whether the machines ever halt. The halting question for the Cryptids remains open.
That means it would be wrong to say the AI "solved" Busy Beaver or BB(6). What has been achieved is a form of structural understanding of machines that were previously fog: where there was once a machine impossible to simulate and without a description, there is now a verified rule that accelerates analysis of its behavior. Which rule applies to which machine, and exactly what is proven in Lean for each one, cannot be confirmed beyond what the source text states.
Openness and Follow-Up
The proof artifacts have been released publicly, making the results checkable and reproducible for anyone who can read Lean. Cryptobriefing also reports that community follow-ups came within days of publication — the source is vague about what these follow-ups involve, and AIMag cannot specify them further.
This openness is part of the point. A benchmark result can be reported and forgotten; a set of checkable Lean proofs can be built upon, refuted, or strengthened by others.
What This Says About AI-Driven Mathematics
This story is not primarily a result about the strength of the AI model, but about a way of working: the system explores, formulates conjectures, and submits those conjectures to a formal judge. The model need not be reliable; the proof assistant is.
It is worth keeping three things separate:
- Verified: Eleven six-state Turing machines have new, Lean 4-checked acceleration rules, based on the preprint released October 15, 2026.
- Attributed, but not independently confirmed: That Gemini generated the proofs is the preprint's own account, relayed by Cryptobriefing. AIMag does not have access to the preprint itself and has not independently verified the attestation process.
- Open: Whether the Cryptids halt remains unanswered. It is this question that ultimately drives BB(6).
One further caveat about the sourcing situation: everything in this story rests on a single secondary article, built on the preprint. The consistency of the numbers — 1,094 examined, 52 flagged, eleven with new verified results — is as given in that coverage.
The Road Ahead
The next step for the Cryptids is what has always been the goal: settling the halting question for each individual machine, which would either push the BB(6) value further up or prove that a given machine never halts. The new acceleration rules are a tool for that work, not its conclusion. And methodologically, the result points toward a pattern that could be repeated on other frontiers in mathematics: AI systems producing conjectures in volume, and formal proof assistants separating what holds from what merely sounds good.