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 条相关)→
「研究」频道最新
- WISD:用弱化版模型蒸馏出训练信号,无需特权数据 — jet-ai · 2026-10-31
- 生物预印本承认用LLM比例三年涨至17%,直追专业AI工具 — teortaxesTex · 2026-10-31
- StudentBench 作者：AI 家教提升人类智力是模型厂商最该主攻的方向 — gharik · 2026-10-31
- ColmapView 开源 Spatial Hub:聚合近 5000 个公开空间数据集 — janusch_patas · 2026-10-31
- ARC Prize 2026 截止倒计时3天,Yi-Chia Chen 以 75.56% 登顶 ARC-AGI-3 — GregKamradt · 2026-10-31
- NVIDIA Nemotron 3.5 用 LLM 自验证:agentic 基准提升 9-10 个点 — sarahcat21 · 2026-10-31