Rohan Paul· @rohanpaul_ai · X·· 4 天前AI 评分61
AI 导读
Google DeepMind 与剑桥大学联合发布论文，展示了一种基于 Gemini 的 agent 工作流，可自主发现并经 Lean 形式化验证了 11 台未解决的 Busy Beaver 图灵机的数学规则。该系统能够通过模拟器测试边界情况、起草非正式证明，并在 Lean 证明检查器中完成形式化验证，标志着 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.
来源：Rohan Paul · x.com