Lean formalization of claimed Navier-Stokes blow-up questioned: is compact support of the force assumed or proved?
Illustrious-Bench726 · reddit · 2026-09-12
A Reddit user scrutinizes the recent Lean formalization of a claimed finite-time blow-up for 3D Navier–Stokes with forcing, raising a key logical question about compact support of the force.
Key observations:
- The formalization's CandidateProperties includes forcetimesupport : CompactFutureTimeSupport f, while a comment says spatial support need not be compact; an "OPEN: the primary existential content…" note indicates no proof, witness, or axiom asserting the proposition exists in that module.
- The author asks four questions: (1) Is compact support of f actually proved by the layer construction in the analytic paper, or assumed to fit versions C/D of the Millennium problem? (2) If proved, which Lean file/module proves CompactFutureTimeSupport f? (3) If assumed, the result only shows "if a singular forced solution exists, then…", which wouldn't resolve Millennium versions C/D by itself. (4) Is there an explicit invariant keeping the force support inside a fixed compact set as layer index grows?
The author stresses they aren't claiming the result is wrong — they want clarity on the exact logical status of compact support in the formalization, since public claims suggest the Lean proof establishes it while the code structure appears to postulate it.
Related event: OpenAI's Navier-Stokes Proof Passes Rechecks but Faces Scrutiny(2 posts)→
More from Research
- How do you benchmark recall for research agents without a gold-standard crawler? — Spirited-Cheek8436 · 2026-09-13
- One Layer Deeper draws 15,000 submissions, none solved as intended — marksaroufim · 2026-09-13
- Researcher argues reward is the optimization target for deeply RL-trained models — jessi_cata · 2026-09-13
- DeepLeap's DELE-w0.5 ditches video-generation pipelines for robot manipulation — jiqizhixin · 2026-09-13
- Generative AI collapses information diversity while engagement algorithms amplify extreme tails — abenitezburraco · 2026-09-13
- New article: Intelligence Has a Speed Limit — why RSI can't run as fast as you like — NathanpmYoung · 2026-09-13