AI 导读
Google DeepMind 与剑桥的论文介绍一个基于 Gemini 的智能体流程，自主发现并形式化验证了 11 台此前无文献分析的 Busy Beaver 图灵机的新规则。该流程先在模拟器中测试边界情况，起草非形式证明，再在 Lean 证明检查器中完成形式证明，作者称显示 AI 可从回答人类设定的数学问题走向开放式发现。
推荐理由
论文展示了 AI 智能体从解答人类提出的问题走向开放式数学发现的路径，流程结合模拟器、非形式证明与 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.
来源：Rohan Paul · x.com