Cardano创始人Charles Hoskinson在9月9日的视频直播中表示，人工智能在形式数学领域取得的进展超出了他的预期。这一表态源于OpenAI此前宣布其内部系统已提出Navier–Stokes千禧年大奖问题的一个解决方案。
Hoskinson将所报道的能力称为“相当了不起”，但他同时指出，这项工作的原始出处以及提交至云端AI服务的研究数据是否仍保持隐私，都是尚未解决的问题。Hoskinson原本预期的是，形式化系统能够帮助大型数学家团队协作，并对人工编写的证明进行验证。他并没有预料到大型语言模型会这么快就自行生成完整证明。“我们从未预见到AI会介入到这种程度，”Hoskinson说。他补充称，此前“AI完全写出一个证明”的想法看起来还很遥远。
Hoskinson与形式数学研究有直接关联。2021年，他向卡内基梅隆大学捐赠2000万美元，成立了Hoskinson形式数学中心。他的最新评论也与Cardano在人工智能层面的广泛实验相吻合。据crypto.news此前报道，Hoskinson曾为Cardano AI智能体实验进行辩护，相关实验涉及通信、社区活动以及注重隐私的Midnight生态系统。
OpenAI于9月8日发表了其研究结果。该公司表示，一个内部模型协调了约1万个智能体，历时88小时产生了一个拟定解。随后，GPT-6 Astra又用了17小时以Lean语言对该论证进行形式化和检查。该证明试图确立：在受到光滑外力作用时，初始光滑的静止流体可在有限时间内形成奇点。OpenAI称，这一结果满足千禧年大奖官方表述中的C和D两项陈述。OpenAI还发布了一篇分析论文和Lean代码。Lean形式化能够提供机器可检查的验证，确保编码步骤确实由所列假设推导而来，但它并不能独立地证明每个定义和假设都精确对应原始数学问题。OpenAI表示并不打算领取相关的100万美元奖金，但仍将该工作描述为“对问题的解决”。
克莱数学研究所仍将Navier–Stokes问题列为“未解”。截至报道时，其网站尚未认可OpenAI提出的证明是已被接受的解答。克莱研究所不接受直接提交的解决尝试。按规则，解答须先发表在符合资格的出版物上，之后至少经过两年，并获得全球数学界的普遍接受。因此，OpenAI的公告和Lean形式化尚不等于即时的机构认可。数学家仍需检验其构造是否满足精确的问题表述，以及使用外力是否真正回答了通常理解下的问题。
这项公告还引发了出处争议。纽约大学数学家Tristan Buckmaster和Anthropic研究员Levent Alpöge此前正在研究一项使用外力方法的Euler方程相关结果。Buckmaster质疑，提交到OpenAI Codex系统的私人工作是否可能对该公司的结果产生了影响。他并未声称已证明存在不当行为，只说：“我不知道我们的数据是否被使用。”OpenAI否认接触过他们的具体工作，但表示不能完全排除其产品使用中产生的去标识化数据可能帮助了模型改进。OpenAI坚称，其证明是独立开发的，并且与上述研究者的工作不同。
Hoskinson认为，这一争议应促使研究人员对未公开的想法更加谨慎。他说，使用集中式AI服务的学者应当考虑其提示词、笔记和研究日志是否仍处于保密状态。
下一阶段将进入公开审查。在专家评估假设、且克莱研究所的正式条件得到满足之前，这项成果仍是一个“声称的解答”，而非“已被承认的解决”。