Lean 4 bekrefter: Gemini-agent beviste regler for elleve BB(6)-maskiner
En Gemini-basert agentsystem fra Google DeepMind og forskere med tilknytning til Cambridge har funnet og formelt verifisert akselerasjonsregler for elleve seks-stats Turing-maskiner som ingen hadde analysert før. Preprinten ble lagt ut på arXiv 15. oktober 2026, og korrektheten hviler ikke på tillit til modellen, men på Lean 4-bevisassistenten. Men spørsmålet som faktisk driver BB(6)-feltet – om maskinene noensinne stopper – er fortsatt åpent.
Nyheten
Ifølge en preprint med identifikator arXiv 2610.22603, lagt ut 15. oktober 2026, har et agentbasert system bygget på Gemini oppdaget kompakte matematiske akselerasjonsregler for elleve tidligere uanalyserte seks-stats Turing-maskiner. Systemet beviste deretter reglene formelt, i et format som enhver skeptiker kan sjekke linje for linje, slik Diego Almada Lopez gjengir det i Cryptobriefings dekning fra 22. oktober 2026, som bygger på preprinten.
Forskerteamet inkluderer Google DeepMind-forskerne Marco Dos Santos, Tom Zahavy og Vivek Veeriah, som arbeider med tilknytning til University of Cambridge. Kildegrunnlaget angir ikke navngitte Cambridge-medforfattere eller den eksakte tilknytningsstrukturen, og dette er ikke bekreftet uavhengig av preprinten.
Presseomtale fulgte 22. oktober, og bevisartefaktene er gjort offentlig tilgjengelige. Det gir feltet – og alle andre – muligheten til å gå gjennom det som faktisk er bevist, ikke bare ta imot en konklusjon.
Hvorfor BB(6) er en front
Busy Beaver-funksjonen spør, for et gitt antall tilstander, hvor lenge den lengst kjørende Turing-maskinen som faktisk stopper, kan kjøre før den stopper. For hver økning i antall tilstander eksploderer vanskeligheten: Maskinene må analyseres én for én, og en håndfull av dem oppfører seg så innviklet at standardmetoder ikke rekker frem. De uanalyserte seks-stats-maskinene – «holdoutene» ved BB(6)-fronten – er akkurat slike gjenstridige tilfeller.
De elleve maskinene denne preprinten handler om, har fått den uformelle betegnelsen «Cryptids»: maskiner som man vet eksisterer, men hvis oppførsel ingen har kunnet beskrive ordentlig. Det er mot denne fronten systemet ble rettet.
Hvordan systemet arbeider
Trakten er konkret: Systemet undersøkte 1 094 BB(6)-holdouts, flagget 52 av dem som verdt dypere studier, og endte opp med nye verifiserte resultater for elleve maskiner som ikke var analysert tidligere, ifølge Cryptobriefings gjengivelse av preprinten.
Metoden går gjennom tre trinn. Først kjøres simuleringer av maskinene. Deretter genereres formodninger – kompakte akselerasjonsregler som beskriver hvordan maskinene oppfører seg over tid. Til slutt konstrueres formelle bevis for disse formodningene i Lean 4, et teorembevisprogram. Cryptobriefing beskriver det kritiske punktet slik: Hvis ett eneste logisk steg mangler, avviser Lean beviset fullstendig.
Det er her verdien ligger for tilliten til KI-generert matematikk. En språkmodell kan ta feil, hallusinere eller hoppe over steg uten å vite det selv. Men et Lean-bevis er ikke en påstand – det er et artefakt som maskinsjekkes. Hvis beviset kompilerer, er setningen bevist uansett hvem eller hva som skrev det. Korrektheten hviler på verifikatoren, ikke på modellen.
Grensene: regler, ikke løsninger
Det viktigste forbeholdet er tydelig, slik kilden gjengir preprinten: De nye reglene beskriver hvordan maskinene oppfører seg, men de avgjør ikke om maskinene noensinne stopper. Haltingsspørsmålet for Cryptidene er fortsatt åpent.
Det betyr at det ville være feil å si at KI-en «løste» Busy Beaver eller BB(6). Det som er oppnådd, er en form for strukturell forståelse av maskiner som tidligere var tåke: Der man før hadde en umulig å simulere maskin uten beskrivelse, har man nå en verifisert regel som akselererer analysen av dens oppførsel. Hvilken regel som gjelder for hvilken maskin, og nøyaktig hva som er bevist i Lean for hver enkelt, kan ikke bekreftes ut over det kildeteksten oppgir.
Åpenhet og oppfølging
Bevisartefaktene er offentliggjort, noe som gjør resultatene sjembare og etterprøvbare for alle som kan lese Lean. Cryptobriefing rapporterer også at oppfølging fra fellesskapet kom i løpet av dager etter publisering – kilden er vag om hva disse oppfølgingene innebærer, og AIMag kan ikke spesifisere dem ytterligere.
Denne offentligheten er en del av poenget. Et benchmarkresultat kan rapporteres og glemmes; et sett med sjekkbare Lean-bevis kan bygges videre på, avkrefte eller styrkes av andre.
Hva dette sier om KI-drevet matematikk
Denne historien er ikke primært et resultat om KI-modellens styrke, men om en arbeidsform: systemet utforsker, formulerer formodninger, og leverer formodningene inn til en formell dommer. Modellen behøver ikke være pålitelig; bevisassistenten er det.
Det er verdt å holde tre ting adskilt:
- Verifisert: Elleve seks-stats Turing-maskiner har nye, Lean 4-sjekkede akselerasjonsregler, basert på preprinten som offentliggjort 15. oktober 2026.
- Attribuert, men ikke uavhengig bekreftet: At Gemini genererte bevisene, er preprintens egen fremstilling, gjengitt av Cryptobriefing. AIMag har ikke tilgang til preprinten selv og har ikke uavhengig verifisert attestasjonsprosessen.
- Åpent: Om Cryptidene stopper, er fortsatt ubesvart. Det er dette spørsmålet som i siste instans driver BB(6).
Étt ytterligere forbehold om kildesituasjonen: Alt i denne saken hviler på én sekundær artikkel, bygget på preprinten. Tallenes konsistens – 1 094 undersøkte, 52 flagget, elleve med nye verifiserte resultater – er som oppgitt i den dekningen.
Veien videre
Neste steg for Cryptidene er det som alltid har vært målet: å avgjøre haltingsspørsmålet for hver enkelt maskin, noe som enten løfter BB(6)-verdien videre eller beviser at en gitt maskin aldri stopper. De nye akselerasjonsreglene er et verktøy for det arbeidet, ikke dets avslutning. Og metodisk peker resultatet mot et mønster som kan gjentas på andre fronter i matematikken: KI-systemer som produserer formodninger i volum, og formelle bevisassistenter som skiller det som holder fra det som bare høres bra ut.
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.