Coq-BB5

Coq-BB5 (author: mxdys) proves theorems in Coq (v8.20.1) about Busy Beaver values, including the following results:

Original results:

• BB(5) = 47,176,870, see CoqBB5/BB5/
• BB(2,4) = 3,932,964, see CoqBB5/BB2x4/

Previously known:

• BB(4) = 107, see CoqBB5/BB4/, first proved in [Brady, 1983]
• BB(3) = 21, see CoqBB5/BB3/, first proved in [Lin, 1963]
• BB(2) = 6, see CoqBB5/BB2/, first proved in [Radó, 1962]
• BB(2,3) = 38, see CoqBB5/BB2x3/, first proved in [Lafitte and Papazian, 2007]

Note: the Coq proofs for the previously known results confirm the results but do not reproduce the original proofs.

Structure of the proofs

The proof of BB(5) is the most general one in the sense that:

1. All the other proofs only use subsets of the techniques used to prove BB(5).
2. All the other proofs use the same overall structure as the BB(4) proof, which is itself a slight simplification of the structure of the BB(5) proof.

BusyCoq

For the proof of BB(5) = 47,176,870, Coq-BB5 relies on the busycoq library (author: meithecatte) for proving that some individual 5-state 2-symbol Turing machines, called Sporadic Machines, do not halt. The BusyCoq/ folder contains a partial snapshot of busycoq, i.e. only the proofs that are used in CoqBB5/BB5/.