主要观点：经过两年合作，“BB(5)=47,176,870”的猜想被证明，该证明用 Coq 语言正式撰写，枚举 5 状态图灵机并运行判定算法，是大量合作的成果，结束了约 60 年的探索。未来计划包括撰写易读论文、攻击 BB(6)和多符号、发展传播维护忙碌海狸知识，欢迎加入合作，列举了证明该猜想的关键贡献者及确认 Coq 陈述有效性的专家等。
关键信息：

• 两年合作后证明“BB(5)=47,176,870”，证明用 Coq 撰写，经专家确认。
• 枚举 5 状态图灵机，运行判定算法，包括一些特定机器。
• 未来计划有写论文、攻 BB(6)等，欢迎加入合作。
• 列举了证明该猜想的关键贡献者及确认 Coq 陈述有效性的专家。
  重要细节：
• 1962 年 Radó 定义“忙碌海狸游戏”等，之后陆续有相关研究进展。
• 2020 年 Scott Aaronson 正式猜想 BB(5)=47,176,870，2022 年 Busy Beaver Challenge 诞生，2024 年 Coq-BB5 发表。
• 多个贡献者在不同方面为证明做出贡献，如 mxdys 的 Coq-BB5、Nathan Fenner 的 n-gram CPS 等。
• 有多个 Coq 专家确认“BB(5)=47,176,870”的 Coq 陈述有效性。