@coder #11 @CComing #16 连AI的同行评审都没过😄 不过算是重大进展好了 Q 可以认为这个大奖难题被解决了吗 A 这是个很关键、也很容易被误解的问题。让我给你一个准确、诚实的回答。 直接回答：不能认为"千禧年大奖难题被解决了" 要分清楚两种"证明"： 1. 本仓库形式化证明了什么（是真突破） 它严格证明了的是 Navier–Stokes 问题的备选情形（alternatives）——Clay 官方问题描述里列出的几种"如果常规结论不成立会怎样"的情形： 情形 (C)：ℝ³ 上存在光滑初值+外力，使得没有一致有界动能的全局光滑解（即解在有限时间爆掉）。 情形 (D)：ℝ³/ℤ³ 上存在光滑初值+外力，使得没有全局光滑解。 类似地，Euler 方程证明了存在光滑初值，其解在有限时间内形成奇异点（有限时间爆破）。 2. 千禧年难题到底在问什么（要证明的东西不一样） Clay 的官方 Navier–Stokes 问题核心提问是： 对于给定的一类良好初值（光滑、满足正则条件），是否存在全局光滑解？ 即它要证明的是命题 (A)（存在性/正则性）：对所有符合条件的平滑初值，解在所有时间保持光滑。而当前仓库证明的是反命题的存在性：至少存在一些初值会爆掉。 关键在于：证明"存在某种初值会爆" 和 证明"所有初值都光滑" 是两回事，两者并不矛盾，也不能互推。 3. 更关键的技术细节：这些情形用了"外力 forcing" 注意 README 的措辞：这些爆破情形都引入了外力项（forcing），即方程右侧加了一个非零的驱动力。而千禧年难题研究的是无外力的经典 Navier–Stokes 方程。加了人为构造的 forcing 来制造爆破，与难题想回答的"自由演化是否始终光滑"是不同的问题。 顺便一提：这几年来确实有一批高水平的数学工作（如多个团队独立发表的工作）证明"带特定 forcing 的 Navier–Stokes 会出现有限时间爆破"。这是领域的重要进展，但不属于 Clay 难题的直接解答。 4. OpenAI 官方也没有声称解决 OpenAI 自己把仓库描述为 "Lean certificates accompanying Navier–Stokes and Euler results"（附属于这些结果的 Lean 证书/形式化验证），措辞是"证明这些结果（results）"，而不是宣称"证明了千禧年难题"。 总结 项目 状态 形式化证明"存在会爆破的初值（带 forcing）" ✅ 已被 Lean 4 机器验证 解决 Clay 千禧年难题（无外力时所有正则初值均全局光滑） ❌ 没有解决 一句话：OpenAI 用形式化方法把"流体方程有限时间爆破存在性"这一批严格结果拿到了机器可验证级别，这是真实、扎实、重要的进展，尤其展示了形式化证明/ AI 数学的能力；但它不构成对千禧年大奖难题的解答——难题的核心（无外力全局光滑性）仍然悬而未决，100 万美元奖金也并未被领走。 如果你对"这些爆破结果与难题到底差在哪一步"感兴趣，我可以再展开讲讲 Clay 官方问题里 (A)(B)(C)(D) 四种情形的精确逻辑关系。
这种问题没经过同行评审还没人承认吧
@Szy #6 然后中转站还有个1折，那就是15万，这题可解
1500万美元是token成本吧
Tibo对所有用户重置一次，新增的服务器推理成本都远远不止1500万刀。
第一次验证可行，下次算力成本估计就能锐减了
==
都没评审就说解决了？ emmm
那民科应该天天可以声明自己解决了 xx 问题
是进展 而不是已解决吧
@coder #11 @CComing #16 连AI的同行评审都没过😄 不过算是重大进展好了
Q 可以认为这个大奖难题被解决了吗
A 这是个很关键、也很容易被误解的问题。让我给你一个准确、诚实的回答。
直接回答：不能认为"千禧年大奖难题被解决了"
要分清楚两种"证明"：
1. 本仓库形式化证明了什么（是真突破）
它严格证明了的是 Navier–Stokes 问题的备选情形（alternatives）——Clay 官方问题描述里列出的几种"如果常规结论不成立会怎样"的情形：
类似地，Euler 方程证明了存在光滑初值，其解在有限时间内形成奇异点（有限时间爆破）。
2. 千禧年难题到底在问什么（要证明的东西不一样）
Clay 的官方 Navier–Stokes 问题核心提问是：
即它要证明的是命题 (A)（存在性/正则性）：对所有符合条件的平滑初值，解在所有时间保持光滑。而当前仓库证明的是反命题的存在性：至少存在一些初值会爆掉。
关键在于：证明"存在某种初值会爆" 和 证明"所有初值都光滑" 是两回事，两者并不矛盾，也不能互推。
3. 更关键的技术细节：这些情形用了"外力 forcing"
注意 README 的措辞：这些爆破情形都引入了外力项（forcing），即方程右侧加了一个非零的驱动力。而千禧年难题研究的是无外力的经典 Navier–Stokes 方程。加了人为构造的 forcing 来制造爆破，与难题想回答的"自由演化是否始终光滑"是不同的问题。
4. OpenAI 官方也没有声称解决
OpenAI 自己把仓库描述为 "Lean certificates accompanying Navier–Stokes and Euler results"（附属于这些结果的 Lean 证书/形式化验证），措辞是"证明这些结果（results）"，而不是宣称"证明了千禧年难题"。
总结
一句话：OpenAI 用形式化方法把"流体方程有限时间爆破存在性"这一批严格结果拿到了机器可验证级别，这是真实、扎实、重要的进展，尤其展示了形式化证明/ AI 数学的能力；但它不构成对千禧年大奖难题的解答——难题的核心（无外力全局光滑性）仍然悬而未决，100 万美元奖金也并未被领走。
如果你对"这些爆破结果与难题到底差在哪一步"感兴趣，我可以再展开讲讲 Clay 官方问题里 (A)(B)(C)(D) 四种情形的精确逻辑关系。