Google DeepMind 论文：Gemini 智能体发现并形式化验证 BB(6) 中 11 台未解 Turing 机的加速规则

Google DeepMind 发表了一篇关于利用智能体进行开放式数学发现的重磅论文。

这是我见过的早期、令人兴奋的自主 AI 驱动发现的工作之一。

（收藏一下）

一个基于 Gemini 的智能体在 BB(6)（忙碌贝蒂数问题的当前前沿）中，为十一个未解决的图灵机发现并形式化验证了新的加速规则。

忙碌贝蒂数问题是不可计算的，因此不存在固定的待解问题列表。智能体必须自行挑选机器、从其执行轨迹中发现规律，并提出能一次性概括大量步骤的紧凑规则。

每条提出的规则都要经过非形式化推理和 Lean 证明。只有被证明的规则才会被保留，因此结果不依赖于信任模型的推理。

作者暂且将这些机器称为“神秘生物”（Cryptids）。它们从空白纸带出发的运行现在有了精确、紧凑的描述，但它们是否停机仍是未解问题。

这是一个很好的例子：智能体在自己选择的问题上产出了新的、经过形式化检验的数学结果。

arxiv.org/abs/2610.22603

Chat with Paper: academy.dair.ai/papers/at-th…