论文78°
DeepMind 与 Cambridge 论文：AI 智能体自行证明 11 台未解 Busy Beaver 图灵机的规则
精选理由
DeepMind 和 Cambridge 用 Gemini 做了个智能体，自己发现并证明了 11 台没人算过的 Busy Beaver 图灵机规则，还用 Lean 验证了，过程挺有意思。
Google DeepMind 与 Cambridge 合作发表论文，展示了一个基于 Gemini 的智能体在没有先前分析记录的情况下，为 11 台 Busy Beaver 图灵机发现并证明了新的精确规则。该智能体在模拟器中测试边界情形，起草非形式化证明，再用 Lean 证明检查器完成形式化验证。这标志着 AI 从回答人类提出的数学问题转向开放式数学发现。
原文 · rohanpaul_ai
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.
