精选理由
这篇论文展示了 AI 在数学证明中的实际进展，做形式化验证或数学研究的团队值得关注——它把 LLM 从“讲故事”变成“可验证的候选生成器”，直接解决了幻觉问题。
Google DeepMind 发表新论文，展示 AI 系统 AlphaProof Nexus 能在形式化数学证明中进行搜索，但仅限于精心约束的世界。该系统使用 Lean 证明检查器，让 LLM 不断编辑形式化证明、读取编译器错误并重试，同时维护共享的局部证明池来指导搜索。在测试中，该系统解决了 9 个 Erdős 问题和 44 个序列猜想，并协助优化、图论、代数几何和量子光学领域的问题。失败案例同样有启示性，揭示了 LLM 在数学推理中隐藏错误的方式。该工作并非实现完全数学自主，而是建立了人机协作的新分工：人类选择问题，模型提出路径，证明助手严格验证。
AI 翻译 · 中文
Google DeepMind 发表新论文，展示 AI 系统 AlphaProof Nexus 能在形式化数学证明中进行搜索，但仅限于精心约束的世界。该系统使用 Lean 证明检查器，让 LLM 不断编辑形式化证明、读取编译器错误并重试，同时维护共享的局部证明池来指导搜索。在测试中，该系统解决了 9 个 Erdős 问题和 44 个序列猜想，并协助优化、图论、代数几何和量子光学领域的问题。失败案例同样有启示性，揭示了 LLM 在数学推理中隐藏错误的方式。该工作并非实现完全数学自主，而是建立了人机协作的新分工：人类选择问题，模型提出路径，证明助手严格验证。
Google DeepMind's new paper. Shows that AI can now search formal mathematics proofs, but only inside carefully constrained worlds. The striking result is not that the system “thinks like a mathematician,” but that it kee…