忙碌海狸游戏 (Busy Beaver Game) 是由数学家 Tibor Radó 在 1962 年提出的一个理论计算机科学问题。这个游戏涉及到一种特殊的图灵机，被称为「忙碌海狸」，它们是设计来在一条无限长的纸带上尽可能多地写下「1」的程序。在忙碌海狸游戏中，给定一个正整数，考虑所有具有个状态的图灵机（包括输入字母表和状态转移函数等）。游戏的目标是找到一个图灵机，在给定的空白输入下，它运行时间最长（或者说经过最多的步骤）才停止，同时输出的 1 的数量最大。这个输出的 1 的数量就是该正整数对应的忙碌海狸函数的值，用 BB(n) 表示，其中 n 是图灵机的状态数。
在 2024 年 9 月，一个由 20 多名贡献者组成的团队宣布他们找到了第五个忙碌海狸数 BB(5)，其值为 47,176,870 。这个结果是由 Tristan Stérin 发起的「忙碌海狸挑战」项目的一部分，该项目是一个在线合作，旨在最终确定 BB(5) 的值。这个团队使用了一款名为 Coq 证明助手的软件来验证他们的发现，这是一个形式化验证工具，用于确保数学证明的准确性。