NS Check
NS Check independently reviewed OpenAI’s claim that smooth fluid flow can break down in finite time. Follow five recorded checks on the proof written in Lean.
Source not currently publicRecorded research exhibit
What each check establishes
Recorded audit ·
OpenAI’s proof concerns fluid flow under a smooth external force. The audit checked two cases of breakdown from Clay’s problem. Alternative C covers all of three-dimensional space. D covers flow that repeats in space.
Open a check to see what the recorded run established and where its evidence stops.
Did the proof compile?Target build · Recorded result: passed
Lean compiled the part of the project that contains the two breakdown proofs.
Limit: Build success alone does not establish statement correspondence.
Did the statements match the reference?Statement and primitive comparison · Recorded result: passed
Comparator matched the two compiled statements to their reference versions in Lean. It also checked the declarations those statements rely on, including Lean’s built-in primitives.
Limit: Manual correspondence with the mathematical problem remains a separate review.
Manual correspondence review
The source assessment reports no mismatch in its manual statement correspondence review. There is no separate specialist sign-off.
What assumptions does it use?Axiom closure · Recorded result: passed
An axiom is a starting assumption accepted without proof. Across the two checked results, the audit recorded only three axioms: propext, Classical.choice, Quot.sound.
Limit: This is an axiom check for the selected roots, not a trust-free foundation.
Did another checker accept the export?Nanoda · Recorded result: accepted
Nanoda, a separate implementation of Lean’s proof checker, accepted the exported proof data.
Limit: Checker implementation and the execution environment remain trusted.
Could Lean check the exported proof again?Lean replay and quotient postcheck · Recorded result: accepted
Lean’s own proof checker also accepted the exported proof data. The run included a follow-up check on quotients.
Limit: The receipt applies only to the pinned target and retained run.
Numerical work is separate
The source assessment withdraws the historical point/rectangle Volterra tail and W* enclosure claims. Formal replay does not restore those claims. No numerical results are included here.
Trust and limits
- These are recorded results. Preparing this projection does not rerun the build, checkers or proof replay.
- The official Mathlib cache was trusted; the entire library was not rebuilt from source.
- The checkers, checking environment, OS and hardware remain part of the trust base.
- This receipt does not map every clause of paper Theorem 1.1 or independently reconstruct all analytic ideas.
- Forced C/D breakdown does not resolve unforced A/B.
- The receipt does not determine a Clay award or establish general mathematical acceptance.
- Results do not transfer to a later upstream revision.
- The export digest identifies retained bytes; it is neither a signature nor an additional proof check.
Roots, axioms and checker revisions
NavierStokes.Comparator.navier_stokes_breakdown_R3NavierStokes.Comparator.navier_stokes_breakdown_periodic
Axioms: propext, Classical.choice, Quot.sound
- Comparator
19e111e2141cf333c7daff0f64c5f24acc91dd2e- lean4export
cacf989bd75f608700820f6afc595f32e7a99a4d- Nanoda
05055695879dfebb6628a67da88ceca6cd6b0421- Landrun
811cfff51ceaf3d9843708aa6d22e9b84ccac8b4
Retained export and receipt metadata
- Scope
- Navier–Stokes Clay alternatives C and D only
- Run completed
- Upstream revision
8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538
1,071,397,994 bytes
Export SHA-256429d30a8d9110faeb84ae0919b5d1b074f3ceea236254eda104f2007262e492f
Metadata only; the retained export is not included in this package.
Source receipt SHA-256087bdb17135777ec1af0964cb0193200c1473e31a703b82e895b4984453fb8cd
Command receipt SHA-256d4fd94ee1a880d2e5249dc99031bea9ad0cc82dfe095dc13e293ca2e99fdc788
One target, several different checks
The Navier–Stokes equations describe how fluids move. OpenAI released a written argument and a version in Lean, a program that checks mathematical proofs. NS Check examined the September 8 release. See OpenAI’s announcement and Clay’s official problem description.
Comparator checked the proof against reference statements already written in Lean. A separate manual review asked whether those reference statements captured the mathematical conditions Clay set. That distinction matters because a computer can check a proof of the statement it was given even when that statement differs from the question a reader had in mind.
The receipt is an account of a retained run. Opening this page does not execute a proof checker. Its export digest identifies stored bytes; it is not a signature or a claim of mathematical acceptance.
Project details
Added · Updated