BusyCoq contributions

A tiny program can be very hard to understand

A six-state, two-symbol Turing machine has a short transition table, yet its behavior can resist enormous amounts of simulation. A long run without a halt is evidence about that run; it is not a proof that the machine will run forever.

This work contributes formal proofs for individual machines in the Busy Beaver community’s holdout lists. Five merged pull requests contain twelve nonhalting proofs and one halting proof. These are contributions toward classifying particular machines, not a solution to BB(6).

From observed behavior to a checkable statement

The workflow begins with simulation and compressed tape descriptions, then proposes macro rules and an invariant. Each macro rule must be justified by the actual transition table. An invariant must include the reached starting configuration, survive every relevant step and exclude halting.

For several related machines, state renaming or mirroring exposes shared structure. The proofs reuse the common argument while checking each exact transition table and its different starting orbit. Resemblance in a plot is not enough.

The acceptance boundary is concrete: compile against the unmodified upstream framework, check the exact machine literal and top-level theorem, inspect assumptions and run coqchk. The research harness also rejects proof escapes such as admitted lemmas.

What shipped

A useful boundary: halting versus the step count

One accepted machine is calculated to halt after approximately 1.77 × 10^44 steps. The formal theorem proves that it halts; it does not prove that exact number. The step count comes from a separate computation with simulation cross-checks. Keeping those claims separate is part of making the result inspectable.

The halting proof compresses the execution into certified batches. An untrusted procedure proposes a batch; proved guards determine whether that batch can be used. The checker does not need to trust the proposal mechanism. This is an appealing pattern for AI-assisted research: let search be inventive, and keep acceptance explicit.

Attribution and the trust boundary

The merged submissions disclose Claude Code’s role in producing the informal proofs and formalizations. My role was directing the effort, reviewing selected explanations and getting the contributions into the upstream project. The current broader search also uses Codex; its unpublished results are not included in the totals here.

These proofs build on BusyCoq and prior community analyses, with the specific dependencies credited in each pull request. Nonhalting submissions report closed assumptions; the halting submission records the framework’s functional-extensionality assumption. Kernel checking validates a formal statement within that foundation. It does not automatically validate every informal explanation or an extra numerical claim.