10月30日AI行业动态｜AI 攻破 5 道开放量子难题：每道均附 Lean 形式化证明，论文与代码已开源

<div style="font-size:16px;line-height:1.8;color:#2c3e50;letter-spacing:0.02em;"> <h2>今日头条：AI 攻破 5 道开放量子难题：每道均附 Lean 形式化证明，论文与代码已开源</h2> <p>物理超级智能公司 <strong>Physical Superintelligence（PSI）</strong> 宣布，其自研 AI 科研系统在量子信息理论领域取得进展，<strong>解决了开放量子问题目录中的 5 个开放问题</strong>——包括负偏转置态的纠缠不可蒸馏性、真空纠缠与贝尔不等式、CGLMP 贝尔不等式的最优测量、PPT 平方猜想与纠缠破坏、以及量子因果过程的可纯化性。不同于只公布摘要的常规做法，PSI 把论文、<strong>Lean 形式化证明和验证代码全部贴在了 GitHub 上</strong>供学界审查。</p> <p>这批题目本身有多老？它们来自 <strong>开放量子问题（Open Quantum Problems, OQP）</strong>目录——该目录由德国物理学家 Reinhard Werner 于 1999 年建立，专门收集量子信息学界长期卡住的重要研究问题，距今已有 27 年历史。其中 OQP 2、OQP 12、OQP 27 三题在本世纪初就已收录。也就是说，PSI 攻下的不是新近提出的小问题，而是这个领域里被反复啃了几十年、始终没人给出完整解答的硬骨头。</p> <p>PSI 的方法论比结果本身更值得研究。其自研系统名为 <strong>Emmy</strong>（致敬数学家与理论物理奠基人艾米·诺特），核心设计是<strong>把"生成"与"验证"彻底分离</strong>：面对一个宏大的物理开放难题，先调用前沿大模型将其拆解成大量微小的、可验证的数学子假设；再把每个假设直接送进 Lean 形式化证明器、符号计算引擎与高精度验证代码中严格筛查——报错的假设当场淘汰，通过局部验证的路径被保留并继续衍生。最终只要 Lean 代码编译通过，就意味着该定理在数学逻辑上无懈可击；而过程中积累的验证结果，还能作为训练下一代"AI 物理学家"的奖励信号。PSI 把这种基本研究单元称为"自主研究任务"（Autonomous Campaign），目标是让研究从问题定义、假设提出、验证、实验到工程部署持续运行。</p> <p>创办人 Alex Wissner-Gross 是一位在 MIT 同时读完物理、电气工程和数学三个本科专业、并以工程学院年级第一毕业的人——MIT 在他之后取消了"同时读三个专业"的选项，理由是"能这么干的人太少了"。他 2007 年在哈佛取得物理学博士学位，早在 2013 年深度学习尚处起步阶段时，就已在 TEDx 舞台上用物理学中的"因果熵力"解释智能行为，主张"智能可以理解为一种不断增加未来行动可能性的倾向"。他今年提出的构想相当直白：<strong>"Solve Everything"</strong>——2026 年 2 月的两篇论文里写下了"证明的时代已经到来"。PSI 于 9 月 1 日公开亮相，宣称要建成"世界上最先进的物理研究实验室"，并已完成 5800 万美元种子轮融资，由比尔·盖茨创立的 Breakthrough Energy Ventures 领投，跟投方包括 SV Angel、a16z 前合伙人 Balaji Srinivasan，以及来自 OpenAI、英伟达、Hugging Face、Oracle 的个人投资者。</p> <h2>行业速览</h2> <ul> <li><strong>Anthropic 将 Claude 送进药厂，文件审查时间缩短近九成</strong>：Anthropic 生命科学团队与六家机构建立深度研究合作，并收购了由单人运营的生物技术公司 Mithril Medicine 直接下场做药。数据显示，Enveda 的制造化学家此前有多达 75% 的工作时间耗费在文件处理上，接入 Claude 后，对 1061 页文件的测试中 Claude 识别出了人工审查员发现的全部 11 个问题、并额外标记出 7 个被人工遗漏的问题，人工审查时间从逾 25 小时压缩至不足 3 小时。Claude 还起草了两份监管文件，其中一份耗时 4 小时，而人工完成同类工作通常需要约 3 个月。Generate Biomedicines 用 Claude Code 提出的 CAR-T 设计方案中，有一个将关键遗传指令片段缩短约 70%，实验室测试显示免疫细胞产生的受体数量约为原来的 10 倍。</li> <li><strong>OpenAI 双倍 Pro 计划使用限额，正面迎战 Anthropic</strong>：OpenAI 宣布双倍多个付费层级的使用限额，Work 与 Codex 配额在 Pro 100 和 Pro 500 计划上均翻倍，Pro 200 的下限配额也翻倍并恢复了原计划削减。时机恰在 Anthropic 准备 IPO 之际，两家公司正在 B2B 领域展开激烈争夺。</li> <li><strong>SK 海力士预警：内存供应短缺或持续到 2030 年</strong>：SK 海力士在第三季度财报中表示，受先进制程技术难度提升及新建生产设施耗时较长等因素影响，存储市场供不应求格局预计将持续至 2030 年。公司称截至 2029 年的三年内其 DRAM 与高带宽内存（HBM）产能实际上已全部售罄，并已与包括全球云服务提供商在内的 14 家主要客户签署长期协议，锁定数量相当于 2027 年和 2028 年总产能的一半以上，合同期限通常为五年。</li> <li><strong>Anthropic 研究：专家会把 AI 的随机意见当成自己的想法</strong>：Anthropic 最新研究发现，领域专家在与 AI 智能体交互时，容易将智能体给出的随机意见采纳并误认为是自己的独立判断——这对"AI 辅助决策"这一正在普及的协作模式提出了一个少被提及但相当关键的认知偏差风险。</li> <li><strong>Claude API 单次请求大小上限提升四倍至 128MB</strong>：Anthropic 将 Claude API 的单次请求大小限制从 32MB 提升至 128MB，面向图像密集型工作负载，使 Claude 能处理更复杂的视觉与多模态任务。</li> <li><strong>OpenAI 扩大与 Oracle 合作，AWS 剑指万亿美元业务</strong>：OpenAI 与 Oracle 扩大合作，Oracle 应用将直接集成进 ChatGPT；亚马逊 CEO Andy Jassy 则表示 AWS 将成为 1 万亿美元业务，但前提是首先需要大量资本支出。</li> </ul> <h2>行业意义</h2> <p>今天这条消息的真正分量，在于它和过去一周另一条新闻形成了某种呼应。前几天，业余数学家借助 ChatGPT 攻克了埃尔德什第 205 号难题，同样用 Lean 做了形式化验证；今天，PSI 把同一套"生成 + 形式化验证"的流水线搬到了量子信息理论，并且一次批量拿下 5 道 27 年历史的开放问题。<strong>两件事指向同一个转折：AI 正在把基础科学的发现能力从"天才手工作坊"改造成"可规模化的工程流程"</strong>。</p> <p>PSI 自己的表述很直白——"让科学发现从天才走向规模化"（From Genius to Scale）。这个提法背后有一个清晰的判断：几百年来基础科学的跃迁几乎全靠牛顿、爱因斯坦式的个体灵光一现，而这种纯手工的科研方式已经撞上天花板；但同时，PSI 也承认，"AI 时代的科研，尽管想法不再稀缺，但真理仍然稀缺"——大模型可以快速生成上百个猜想，但这些离成为真理还差得远。Emmy 把生成与验证分离，正是对这句话的工程回应。</p> <p>这里最值得借鉴的其实不是"攻克了 5 道难题"这个结果，而是<strong>"验证"环节的不可省略性</strong>。一个模型可以写出一段看起来无懈可击的物理论证，但只有当它能在 Lean 里编译通过、在符号计算引擎和高精度验证代码中被筛过一遍，你才有资格说它在数学逻辑上站得住。这套"候选假设批量生成 → 形式化筛错 → 通过者继续衍生"的流水线，本质上把科研里最昂贵的部分——人类专家逐个检查证伪——从"逐篇人工审阅"降维成了"可自动化的编译与判定"。</p> <p>另一个被低估的信号是<strong>开源与可审查性正在成为 AI 科学成果的前置条件</strong>。PSI 把论文、Lean 证明、验证代码连同带时间戳的早期草稿一并公开，甚至提供了校验草稿时间戳的脚本。这与前几天 OpenAI 把三项数学与物理发现的证明交由外部学者独立验证、并在物理一项上主动延后发布形成了呼应——当 AI 产出的成果越来越多，<strong>"谁来判定它为真"这件事本身，就成了核心议题</strong>。</p> <p>对技术团队而言，今天有三条可以直接用起来的判断。其一，<strong>如果你在做需要正确性的工作（财务计算、编译、协议实现、测试断言），把"生成"和"验证"分开设计</strong>——让模型提候选、让编译器或形式化工具做判定，比让模型自己宣布结论可靠得多，这套模式可以直接平移到日常研发里。其二，PSI 已经把自己的商业化路径想清楚了：<strong>先从 AI 数据中心这类"物理极限优化"需求赚钱</strong>——把供电、散热、通信和算力当作一个整体方程求解，从物理层面找更高能效比。这说明 AI for Science 离现金流并不远，约束来自工程落地而非科学本身。其三，<strong>基础科学的开放问题正在变成可批量清扫的存量</strong>，这对做知识工具、检索与教育产品的人是个信号——过去只能靠专家人力长期积累的领域知识，正在被批量转化为"有形式化证明背书的可查询资产"。</p> <h2>消息来源</h2> <p>量子位（经 36 氪授权发布）、Physical Superintelligence 官方仓库 github.com/physical-superintelligence/oqp-batch-2026、华尔街见闻（经新浪网转载）、AlphaSignal、THE DECODER、财联社等公开报道。文中 5 道问题的题号与内容（OQP 2 负偏转置态的纠缠不可蒸馏性、OQP 12 真空纠缠与贝尔不等式、OQP 27 CGLMP 贝尔不等式的最优测量、OQP 38 PPT 平方猜想与纠缠破坏、OQP 43 量子因果过程的可纯化性）及"每道结果含论文与 Lean 4 形式化证明"均以 PSI 官方仓库为准，仓库同时提供带时间戳的早期草稿与校验脚本；开放量子问题目录由 Reinhard Werner 于 1999 年建立，距今 27 年。Enveda 文件审查的页数、问题数与耗时等数据引自 Anthropic 官方发布及其转载报道；SK 海力士的产能锁定与长期协议数据引自其第三季度财报及相关报道。所有成果目前均为预印本阶段，学术解读与影响评估有待学界独立完成。</p> </div>