DISCO collaborator, Tristan, and his friends over on bbchallenge.org have settled the 5th Busy Beaver number, or BB(5), by finally announcing that they’ve proved BB(5) = 47,176,870. The work includes verifying the proof in the automated theorem-prover Coq, and now Tristan and co are diligently writing up this scientific tour-de-force for ultimate verification and community acceptance via peer review.
Quanta magazine writer Ben Brubaker wrote a fantastic article on the 40-year history of this problem. We urge you to check it out! It gives background including fun anecdotes about the key characters over the past decades, up to and including Tristan’s story about founding bbchallenge.org two years ago while he was a PhD student at Maynooth University.
Here’s a picture of the winning Busy Beaver Turing machine’s execution, each line in the image corresponds to a step of the machine, starting at the top and ending at the bottom after 47,176,870 steps. The machine works in binary: 1s in white, 0s in black. You’d never guess from this image that it halts!
