#GoogleDeepMind##AlphaProof##AI数学##形式化证明#
【行业动态：AlphaProof Nexus解决开放数学问题，AI证明搜索能力继续被验证】
Google DeepMind推出AlphaProof Nexus，把大语言模型生成证明和Lean形式化验证结合起来，用AI智能体搜索数学证明。最新信息显示，这套系统在353个开放的Erdős问题中自主解决了9个，其中包括2个悬置56年的问题；它还在OEIS的492个开放猜想中证明了44个，并解决了1个存在15年的Hilbert函数问题。
这类研究的关键，是把AI数学能力放进可验证环境中。Lean形式化系统会逐步检查每一步证明是否合法，避免模型只生成看似合理的自然语言推理。AlphaProof Nexus由多个复杂度不同的智能体组成，有的只依赖Gemini 3.1 Pro和Lean反馈循环，有的则加入AlphaProof和类似AlphaEvolve的进化机制。数学AI正在从“给出答案”走向“在编译器反馈中搜索可验证证明”。