DeepMind 论文：Gemini agent 在 Busy Beaver 前沿自主发现并 Lean 验证 11 条新规则
rohanpaul_ai · x · 2026-10-22
Google DeepMind 与剑桥的论文《At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier》（arXiv:2610.22603）展示了 AI 从解答人类出题走向开放式数学发现的一步。
要点：
- 领域选择：Busy Beaver 是不可计算的前沿——不存在对每个 n 都能算出 BB(n) 的算法，天然适合持续探索式猜想与证明，超越静态、人类预设的问题集。
- 方法：基于 Gemini 的 agentic 流水线，整合模式识别、自动猜想、非形式化数学推理与 Lean 形式化定理证明，自动发现图灵机的「加速」规则（以紧凑数学规则概括大量执行步骤）。
- 成果：系统自主发现并形式化验证了 BB(6) 中 11 台此前无记录分析的机器的新型 Collatz 类加速规则，并在模拟器中测试边界情况；待社区接受后暂定归类这些结果。
- 作者含 Marco Dos Santos、Tom Zahavy 等。
所属事件:DeepMind 联手剑桥：AI 智能体发现并验证 Busy Beaver 新规则(3 条相关)→
「漫话AGI」频道最新
- 安全研究者押注开源模型： plurality 才是 AI 防御的出路 — ziv_ravid · 2026-10-22
- François Fleuret 定义「理解」:所有无意识一致性检查都不报警 — francoisfleuret · 2026-10-22
- Axios 独家：美国大行发现客户账户内潜伏未授权第三方 AI 代理 — daniel_mac8 · 2026-10-22
- OpenAI 宣称攻克 Navier-Stokes 后，哈佛数学家激辩 AI 证明价值 — rohanpaul_ai · 2026-10-22
- ARK 分析师：算力固然稀缺，但数据才是真刚需 — skorusARK · 2026-10-22
- RISC-V 之父 David Patterson：全民高收入是 AI 时代最可能结局 — davidpattersonx · 2026-10-22