原文核完：arXiv:2610.22603，2026-10-15 提交，标题 At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier。七位作者，Marco Dos Santos 领衔，Tom Zahavy 压阵。
帖子的每个关键点都躺在摘要里：Gemini-based agentic pipeline；自动发现图灵机的「加速」——用紧凑数学规则概括大量执行步骤；集成模式识别、自动猜想、非形式数学推理与 Lean 形式定理证明；BB(6) 里十一台机器的类 Collatz 加速；自主发现并经形式化验证；Cryptids 的暂定分类——空白纸带执行有精确紧凑的数学描述，但停机行为仍未解决；推进 BB(6) 遗留机器的分析。
有个细节值得单独说：帖子标题里的「捡到」其实比论文自己还保守。论文的措辞是 advance the analysis of BB(6) holdouts——这十一台机器本来就是 BB(6) 名单上的遗留户，AI 做的是给其中十一台找到了「加速」这条紧凑描述。是发现新结构，不是发现新机器。
Lean 那一环是硬门槛：没有形式化验证，这些「加速」只是漂亮的猜想；验了，才配叫数学。这也是全文最该被圈出来的地方——在不可计算的地基上，可计算的楼是一层层盖起来的。
卡上画的就是这一幕：深夜的纸带缓缓滚动，小机器人在上面跋涉；纸带下面聚着十一头肚皮上刻着希腊字母的小怪兽，每头顶着一个问号——被精确地描述，停不停没人知道。