近期 AI 在数学领域取得突破——从奥林匹克奖牌级别的解答到解决长期悬而未决的猜想——显著提升了自动化系统的能力。但这些成果大多针对预先设定、由人类构造的问题，尚未展示 AI 如何自主发掘数学结构并提出新问题。
忙碌的啄木鸟（Busy Beaver，BB）问题是一个不可计算的前沿，它对每个 $n$ 的 BB 数 $\mathrm{BB}(n)$ 都不存在通用算法。因此，它提供了一个天然的、开放式的探索空间，适合通过猜想与证明进行持续研究。
本文提出了一套基于 Gemini 的主体化流水线，能够自动发现图灵机的加速规则——即用紧凑的数学表达式概括大量执行步骤。系统包括模式识别、自动猜想、非形式数学推理以及在 Lean 中的形式化定理证明四个模块。
在该框架下，系统自主发现并在 Lean 中形式化验证了 $\mathrm{BB}(6)$ 中十一台机器的类 Collatz 加速规则。这些机器的空带运行可以用精确、简洁的数学描述，但其停机行为仍未解决。
我们暂时将这些机器称为 “Cryptids”，即其执行过程可被完整描述却未知是否停机的图灵机。该分类有助于组织 BB(6) 的剩余难题，并为后续研究提供明确目标。
这些成果展示了自主 AI 在基础计算科学中进行开放式数学发现的潜力，标志着从静态挑战向动态探索的关键转变。
点评