AlphaProof Nexus 在 353 个开放 Erdős 问题上大规模 formal proof search：自主解决 9 题，并证明 44/492 个 OEIS 猜想

Google DeepMind 等发布 AlphaProof Nexus，用 LLM agents、Lean compiler feedback 与 evolutionary coordination 在 research-level open problems 上做大规模 formal proof search。论文报告 full-featured agent 自主解决 353 个开放 Erdős 问题中的 9 个，其中两个已开放 56 年；还证明 492 个 OEIS conjectures 中的 44 个，并解决 algebraic geometry、convex optimization 等研究问题。作者公开 Lean proofs 与部分自然语言 writeups；basic agent 也能复现 9 个 Erdős successes，但在难题上成本更高。