“They’ve finally verified the true value of a number called BB(5), which quantifies just how busy that fifth beaver is.”
BB(5) is 47,176,870. Heiner Marxen found the machine that runs that long in 1989. Proving nothing with five rules runs longer took 35 more years and a crowd of more than 20 contributors, most without academic credentials. Georgi Georgiev got it down to 43 holdouts in 2003 with 6,000 lines of uncommented code and then burned out. The amateurs finished it with Coq, which is why anyone believes them.