RecodeX 重构消息，谷歌DeepMind的AI数学证明框架AlphaProof Nexus的研究成果登上《Science》，该框架由Gemini驱动，采用“Gemini写证明、Lean检查、报错反馈修改”的循环流程。

研究从353道已有Lean形式化版本的问题中选出题目进行尝试，最终解决9道埃尔德什开放问题，其中Erdős #12悬置56年、Erdős #125悬置30年、Erdős #846悬置34年。此外还证明了OEIS整数序列百科中的44个猜想，解决一道搁置15年的代数几何难题，并改进了凸优化领域一个沿用已久的理论边界。

论文共有20位作者，其中包括AlphaGo核心研究员Aja Huang。整套Lean证明代码已公开。