谷歌 DeepMind 于 5 月 24 日发布了一篇论文，介绍了一种名为 LLM-Lean 的智能体循环系统。该系统能够自主解决 353 个未解决的埃尔德什问题中的 9 个——其中部分问题已悬而未决超过 50 年；同时还成功证明了 492 个待验证的 OEIS 猜想中的 44 个，每个问题的解决成本仅几百美元。该系统的详细内容可查阅 arxiv.org/abs/2605.22763。它把用于生成证明的大型语言模型与 Lean 形式化验证编译器相结合，后者会对每一个逻辑步骤进行机械式校验，只有在 Lean 确认证明无误后才会交由人类审核。这个智能体还解决了代数几何领域一个存在了 15 年的难题，并发现了优化理论中一个全新的算法参数。
论文的核心发现是：只要让智能体周期性地执行“大型语言模型生成内容→编译器反馈校验”的流程，就能复现全部 9 个埃尔德什问题的解决成果；而加入了进化搜索与强化学习功能的完整系统仅在处理最棘手的问题时才具备优势，这一结果说明提升基础模型的能力或许比增加架构复杂度更为关键。对失败案例的分析显示，这类人工智能常会凭空编造辅助引理，或把核心难点包装成辅助性引理来掩饰；而 Lean 编译器能自动识别这些错误，非形式化的证明方法则难以做到这点。目前这类方法的成功案例多集中在组合数学、数论及优化领域，这些领域的 Lean 数学库（Mathlib）最为完善；需要构建全新理论体系的问题目前仍无法被解决。
加里·马库斯指出这种方法是神经符号型技术，称其比 OpenAI 的非形式化证明研究“更严谨且更具量化依据”，这也引发了人们的疑问：OpenAI 是否知晓 DeepMind 即将发布研究成果，才匆忙发布了自家的相关公告？内特·索雷斯则认为尽管这项成果意义重大，主流媒体却大多对其视而不见，他把这归咎于社会面对具有变革意义的人工智能发展时处于“梦游状态”。这篇帖文在发布 24 小时内便获得了 260 万次浏览。