谷歌DeepMind用Gemini Agent发现BB(6)图灵机加速规则并完成形式化证明

谷歌DeepMind团队发表的一篇关于开放式数学发现的研究论文，在科研智能体领域取得了颇具价值的进展。

该团队借助基于Gemini开发的智能体工具，针对繁忙海狸问题中的BB(6)前沿课题，为11台停机状态尚未明确的图灵机找到了全新的加速规则，并且完成了Lean系统的形式化证明核验。

这项研究的核心流程是，系统会从待解的图灵机中自主选定研究对象，通过分析其执行轨迹中的重复模式，提炼出能够一次性概括大量操作步骤的紧凑数学规则。

在生成规则后，研究团队还会对规则进行进一步的逻辑推理，再提交给Lean证明核验系统进行验证。只有通过核验的规则才会被保留，确保结论的正确性。

研究人员目前将这些尚未明确停机状态的图灵机归为“Cryptids”类别，虽然它们从空白磁带启动后的运行过程已经有了精确且简洁的描述，但最终是否会停机的问题依然没有得到解决。

对于关注科研智能体发展的相关领域从业者来说，这篇研究成果具有较高的研读价值，相关论文可查阅对应学术平台的公开链接。