Machine-checked BBB(4) in Coq: every 4-state 2-symbol Turing machine quasihalts by 32,779,478 or never quasihalts. One axiom.
coq turing-machines formal-verification bbb busy-beaver bbchallenge beeping-busy-beaver quasihalting
-
Updated
Sep 9, 2026 - Rocq Prover