Google DeepMind Team Uses Lean to Verify 11 Busy Beaver Descriptions

Researchers at Google DeepMind and the University of Cambridge used an AI system to formalize the behavior of 11 six-state Turing machines in the BB(6) set. The work provides a compact description of each machine’s behavior, but does not resolve whether any of the 11 eventually stops. The descriptions cover runs that begin with a blank tape. They condense behavior that might otherwise take many steps to trace into rules that can be checked by a computer. Lean 4 checked formal proofs of those rules. Verifying a machine’s described behavior does not establish whether it ultimately halts or continues indefinitely.

Source: TokenPost