Tag
Google DeepMind and University of Cambridge researchers present a Gemini-based agentic pipeline that autonomously discovers and formally verifies novel Collatz-like accelerations for eleven Busy Beaver BB(6) machines, integrating pattern recognition, automated conjecturing, and Lean theorem proving to advance open-ended mathematical discovery.
A GitHub repository presenting machine-checked Coq proofs of new Busy Beaver champions, including a 10-state machine whose score exceeds Graham's number (f_{ω+1} level in the fast-growing hierarchy), beating the previous BB(8), BB(9) and BB(10) champions with exact scores verified without axioms.