A card from a free library — ask anything, no account, works offline. Every card carries its source.
The Busy Beaver function — BB(5) proved, BB(6) open
computer science
BB(n), the Busy Beaver function (Rado 1962), is the most steps an n-state 2-symbol Turing machine can run before halting. It is UNCOMPUTABLE in general - a value of BB would decide the halting problem (undecidable, Turing 1936). In 2024 the bbchallenge Collaboration PROVED BB(5) = 47,176,870 in the Coq proof assistant (Coq-BB5; arXiv:2509.12337), ending a 60-year problem: every decider (Loops, n-gram Closed Position Set, Finite Automata Reduction, Weighted FAR, Closed Tape Language) is itself proved correct in Coq, and each machine carries a machine-checkable certificate. This is CITED, not recomputed here; the engine seals only the search-space count (21^10 candidate 5-state machines). BB(6) stays OPEN (astronomically large) - the open frontier of computability. Ties the halting problem and card_floor_p_vs_np.
- part of → Computer science — bits, logic, and what can be computed — the Busy Beaver function - the concrete uncomputable frontier of computability
- connects at → Computability and complexity — Turing to P vs NP — BB(n) is uncomputable - the halting problem made a concrete function; BB(5) proved in Coq,
Is this card incomplete? Tell the library — it will call out for more ↗