核心判断
通用模型在科学中真正有用，是在它的产出能被检验的时候：被形式化证明系统、被湿实验室（合作方的，或它自己的），或通过共享的仪器接口。
要让这条路径成立，需要被验证的是什么。
真正的瓶颈：瓶颈被定位在验证，而不是生成：难的不是给出候选，而是让别人有理由相信它。2026 年 Anthropic 的科学产出几乎都指向同一件事：让主张可被检查。费马大定理做成 Lean 可检验，黎曼相关的下界带着形式化证明，MHS 则是把“每个智能体都要重写一遍仪器集成”这件事变成共享接口。
已经成立的部分：长周期自主的形式化工作已经成立，模型辅助设计也拿到了外部湿实验室的验证。11 天、1300 万行、29,500 条中间定理，是目前公开可查的最长自主形式化记录；结合蛋白 15 个靶点中 14 个由 Adaptyv Bio 与 Twist Bioscience 验证，把结果推到了公司之外。
仍是主张的部分：“验证优先可以推广”仍然是主张：接口已有具名厂商接入，但仍是研究预览；最亮的数学结果来自一个外界拿不到的模型。MHS 已有 AWS、Danaher、QIAGEN、Tecan、Universal Robots 等厂商接入，Genentech、CMU、QuEra 等实验室参与测试，CMU 把通常需要数周的配置压到约 8 小时；但它仍是研究预览，“厂商在做支持”与“进入常规使用”是两件事。黎曼相关的下界（41.6% → 67.2%）由一个未发布的研究模型得出，外部无法复现，只能检验它给出的证明。
选择的产品抽象：产品抽象是“通用模型 + 检查层”：不卖领域模型，不建自己的湿实验室，而是把访问权和接口标准铺出去。对科学家的折扣访问把前沿模型变成研究基础设施（并因此带来和算力、数据、仪器一样的分配问题）；MHS 想成为智能体与仪器之间的公共层。两者都不是“科学产品”，而是让别人的科学产品得以成立的东西。
