Google DeepMind 与剑桥论文：AI 智能体自主发现 11 台未解图灵机的精确规则
New Google DeepMind and Cambridge paper shows that an AI agent can discover new math itself, proving exact rules for 11 unsolved Turing machines.
AI 导读
Google DeepMind 与剑桥的新论文显示，一个基于 Gemini 的智能体能够自主发现新数学，为 11 台此前没有分析记录的 Busy Beaver 图灵机找到并给出精确规则。该智能体在模拟器中测试边界情况、起草非形式化证明，再在 Lean 证明检查器中完成证明，相关规则均通过 Lean 验证。论文称这体现了 AI 从回答人类提出的数学问题走向开放式发现。
推荐理由
AI 评分 73
该工作展示 Gemini 智能体从回答人类提问转向开放式数学发现，并用 Lean 完成形式化验证。
主题
正文 · AI 翻译
谷歌 DeepMind 与剑桥大学的新论文显示，一个 AI 智能体能够自主发现新的数学，为 11 台未解图灵机证明了精确规则。
AI 能够从回答人类提出的数学问题，迈向开放式发现——一个基于 Gemini 的智能体为 11 台此前没有任何分析记录的 Busy Beaver 图灵机找到并经由 Lean 验证了新规则，证明了这一点。
它在模拟器中测试边界情况，起草非形式化证明，随后在 Lean 证明检查器中证明这些规则。