Coq-BB5 (author: ccz181078/mxdys) proves theorem in Coq about Busy Beaver values, including the following results:
BB(5) = 47,176,870BB(2,4) = 3,932,964BB(4) = 107See the CoqBB5 folder.
Coq-BB5 relies on the busycoq library (author: meithecatte) for proving that some individual 5-state 2-symbol Turing machines do not halt. The BusyCoq folder contains a partial snapshot of busycoq, i.e. only the proofs that are used in Coq-BB5.
Assuming that you have installed Coq, the following command will compile the proof of BB(5) = 47,176,870 (see CoqBB5/README.md for compiling the other results):
make -j 13Replace 13 with the number of cores you want to use. Alternatively you can also run cd BusyCoq && make -j 13 && cd ../CoqBB5 && make -j 13.
The proof will compile in about 45 minutes with 13 cores using native_compute (opam install coq-native) and in about 3 hours using vm_compute and consume in all cases about 4Gb of RAM.
When using native_compute you may have to run ulimit -s unlimited before compiling the proof.