Rohan Paul· @rohanpaul_ai · X·· 2 小时前AI 评分63
AI 导读
Google DeepMind 与剑桥的论文介绍一个基于 Gemini 的智能体流程，自主发现并形式验证了 BB(6) 中 11 台此前无记录分析的 Busy Beaver 图灵机的新加速规则。该流程在模拟器中测试边界情况、起草非形式证明，再在 Lean 证明检查器中完成定理证明；团队暂将这些机器归类为 Cryptids，其停机行为仍未解决。
正文 · 原文
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.
来源：Rohan Paul · x.com