For The Busy Beaver Challenge to be successful we want to formally prove as many of the challenge's results as possible.
This includes:
- Proving the correctness of deciders (https://github.com/bbchallenge/bbchallenge-deciders)
- Proving the non-halting/halting of specific individual machines that are not covered by deciders
Please see our reproducibility and verifiability statement for more.
We elaborate and store these proofs here.
At the moment we focus on writing standard plain-English proofs but future work includes a translation to formal proof systems such as Lean or Coq.
This work is licensed under a Creative Commons Attribution 4.0 International License.
You should have received a copy of the license along with this work. If not, see http://creativecommons.org/licenses/by/4.0/.