Abstract
We're calculating the fifth value of a function... that can't be calculated. This function, called Busy Beaver and proposed by Tibor Radó in 1962, measures the maximum number of operations a program can perform before stopping, as a function of its size. For the first time in over forty years, a new value, BusyBeaver(5) = 47,176,870, has been determined.
The 181,385,789 special cases were formally verified by a computer using the Coq proof assistant, as part of a massively collaborative research effort that mobilized a hundred people on the Internet over a two-year period (bbchallenge.org).
