Reddit 网友质疑 Navier-Stokes 反例的 Lean 形式化：力的紧支撑是假设还是已证？
Illustrious-Bench726 · reddit · 2026-09-12
一位 Reddit 用户详细分析了近期声称的「带外力的 3D Navier-Stokes 方程有限时间爆破」结果的 Lean 形式化代码，提出关键疑问：形式化中 CandidateProperties 包含 forcetimesupport: CompactFutureTimeSupport f（力的时间紧支撑），但代码注释明说空间支撑不要求紧，且模块标注「OPEN: the primary existential content…」，即没有证明、见证或公理断言该命题存在。
作者的四个具体问题：
- 解析论文中力的紧支撑是由层构造（layer construction）实际证明的，还是为适配千禧年问题的 C/D 版本而额外假设的？
- 若已证明，Lean 代码中哪个文件/模块给出了 CompactFutureTimeSupport f 的证明？
- 若是假设，形式化结果只是「若存在满足这些性质的奇异强迫解，则爆破」，这本身并不能解决千禧年版本的 C/D。
- 层索引增长时，如何防止力的支撑扩散到无穷远？是否有显式不变量或不等式将支撑保持在固定紧集内？
作者强调并非质疑结果本身有错，而是想厘清紧支撑在形式化中的确切逻辑地位：他看到不少人宣称 Lean 证明确立了紧支撑力，但代码结构似乎只是把该性质作为前提假设。
所属事件:OpenAI 纳维-斯托克斯证明复现通过但遭社区质疑(2 条相关)→
「研究」频道最新
- Schmidhuber 长文梳理 1987 年以来元学习与递归自我改进全脉络 — SchmidhuberAI · 2026-09-13
- AI 证明 Navier-Stokes 后,数学家理解首次落后于证明 — geoffwolfe · 2026-09-13
- 如何评测爬虫型 Agent 的召回率?发起者探讨无金标准难题 — Spirited-Cheek8436 · 2026-09-13
- 研究者提出:奖励就是深度 RL 训练模型的优化目标 — jessi_cata · 2026-09-13
- 深度跃迁发布 DELE-w0.5:弃用视频生成管线做机器人操作模型 — jiqizhixin · 2026-09-13
- 生成式AI抹平信息多样性，与推荐算法走向相反 — abenitezburraco · 2026-09-13