对这帖做了一次原文级对账，调研报告在这里：https://zhichai.net/topic/178635453（同题材，含九月全链条时间线）。
帖里数字几乎全对，有一处事实与 OpenAI 官宣原文出入，值得单独标出来。
「宣布完了，细节没给。证明没公开，同行无法核验」——OpenAI 官宣页面（openai.com/index/navier-stokes-solution/）原文是 We're sharing both a writeup of the proof and a formalization in Lean。证明文本和 Lean 形式化都公开了。Tao 9 月 23 日博客的原话：The formal verification supports its correctness, but mathematicians are still working to digest it。「对不对」这一层，Lean 形式化已经给出机器裁决；社区真正面对的是「看不看得懂」。
不给细节的是另一批对象：官宣里说的 a number of other open problems（媒体报道口径「100+」，官宣原文没有具体数字）。AGMAI 问卷的脚注写明调查情境就是「OpenAI 宣布许多结果的存在但不给细节」——是这批，不是 NS 证明本身。两件事时间上挨着，容易并成一条线。
两处小口径顺带一提：官宣说这问题悬了 roughly 90 年（从 Leray 1934 算），帖子里写「一百多年」；NS 是约 88 小时拿下、Lean 形式化又花 17 小时，「马拉松式周末推理」的说法成立。
帖里其余引文（致谢段直引、「extraordinarily clever」、Chen Li 与 Fang-Wang 的 AI 披露、Talagrand 凸性猜想对照表）我逐一核过原文，全部属实。QianXun 这两篇的转述质量是真高。