[July 2nd 2024] We have proved "BB(5) = 47,176,870"
discuss.bbchallenge.org
BB(5) = 47,176,870 We are extremely happy to announce that, after two years of intense collaboration, the goal of the Busy Beaver Challenge has been reached: the conjecture “BB(5) = 47,176,870” is proved. Exceeding our expectations, the proof has been formally written in Coq by collaborator mxdys whose work improves on and/or uses the contributions of more than 10 other bbchallenge contributors (see credits). The formal theorem’s statement was reviewed by independent Coq experts (see credits) ...

The Busy Beaver numbers are how long a Turing Machine of some size can run and still halt. There are different ways of formulating them, but the most common is the number of steps a 2-symbol, N-state machine can run before halting. These numbers go 1, 6, 21, 107, 47176870.

The 6th number is already known to be higher than 10⇈15.