据 xinzhiyuan 称，Google DeepMind 于 5 月 26 日发布了 AlphaProof Nexus，这是一款 AI 数学代理，解决了 9 个长期未决的 Erdős 问题，其中最早未解决的已有 56 年。每个解的成本仅为数百美元。

每个证明都由 Lean 编译器进行形式化验证，从而消除了出错的可能性。DeepMind 还报告了在代数几何、凸优化、图论和量子光学方面的突破。