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.
Google DeepMind 与剑桥的新论文显示，一个基于 Gemini 的智能体能够自主发现新数学，为 11 台此前没有分析记录的 Busy Beaver 图灵机找到并给出精确规则。该智能体在模拟器中测试边界情况、起草非形式化证明，再在 Lean 证明检查器中完成证明，相关规则均通过 Lean 验证。论文称这体现了 AI 从回答人类提出的数学问题走向开放式发现。
推荐理由
AI 评分 73
该工作展示 Gemini 智能体从回答人类提问转向开放式数学发现，并用 Lean 完成形式化验证。
主题
正文
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 can move from answering human-posed math questions to open-ended discovery, shown by a Gemini-based agent that found and Lean-verified new rules for 11 Busy Beaver machines with no prior documented analysis.
It tested edge cases in a simulator, drafts informal proofs, and then proves the rules in the Lean proof checker.