Busy Beaver BB(5) Proved

An online collective proves in 2024 the fifth Busy Beaver value (47,176,870 steps), fully machine-checked in Rocq.

The Busy Beaver asks how long the longest-running n-state Turing machine can go before it halts. The function grows faster than any computable function. Marxen and Buntrock found the champion in 1989; the bbchallenge collective proved it optimal in 2024 with a proof formalized in Rocq. BB(6) is open; only astronomically large lower bounds are known.