谷歌 AI 框架 AlphaProof Nexus 攻克 2 道悬置 56 年数学难题

IT之家 5 月 26 日消息，谷歌 DeepMind 最新推出 AlphaProof Nexus，结合大语言模型（LLM）生成证明与 Lean 形式化验证，在 353 个开放的 Erdős 问题中自主解决 9 个，并解开 2 个悬而未决 56 年的问题。IT之家注：Lean 是一种形式化证明语言和证明助手系统。研究者可以把数学命题、定义和证明步骤写成严格可检查的代码，编译器会逐步判断每一步是否合...