AlphaProof Nexus：用形式化验证驱动AI数学证明搜索

研究进展短期未必马上可用，但它常常预示下一代工具能力。普通用户可以把它当作趋势信号，关注后续是否被主流产品采用。

发生了什么

Google DeepMind提出了AlphaProof Nexus系统，它将大型语言模型与Lean形式化验证工具相结合。该系统允许LLM在生成证明的过程中，不断读取Lean的编译错误并进行修正，还可调用更强的工具辅助解决子问题。这一机制迫使模型将每一步逻辑都转化为可编译、可验证的代码，从而将其角色从“令人信服的叙述者”转变为“候选方案生成器”。在针对353个Erdős问题和492个开放猜想的测试中，系统成功解决了9个Erdős问题并证明了44个序列猜想。该研究展示了形式化验证在暴露AI逻辑错误、建立“人类提问-模型探索-验证器把关”新分工中的关键作用。

普通用户需要关注什么

重点看是否有开源实现、是否被主流产品引用，以及是否会在 1-3 个月内转化为可用工具。