Honesty panel
What is not claimed
Aggregated verbatim from the source repositories. This page exists so the honest boundary is visible, not buried.
Across all packages
- None is a claimed solution of a Clay Millennium Problem, and none has Clay Institute recognition or independent specialist review.
- The blow-up mathematics and the Lean formalization are OpenAI’s (NavierStokesAndEuler @
f9e8bc5b, Apache-2.0). GI’s contribution is statement/bridge/packaging/verification. - No proof here was found by the CHAOS system; the Tao proofs are builder-authored.
- No claim is made about Fefferman’s alternatives (A) or (B); they remain open.
- Not independently reviewed or reproduced: every check was run by the package builder on one Linux x86_64 node.
- A PASS line authenticates file bytes and the axiom closure. It does not establish mathematical truth, and it does not show an open premise is true or consistent.
Tao ShortBound — conditional
The result is the implication ShortBound → GlobalRegularityTorus for a local, Fourier-side mild-solution formalization of the periodic Navier-Stokes system. ShortBound (Tao, arXiv:0710.1604) is an open premise that is not proved here. This is not a proof of global regularity, and it says nothing about classical solutions. It is a release candidate, not a tagged release.
Per-package limits: see each repository’s docs/KNOWN_LIMITATIONS.md / KNOWN_LIMITS.md and docs/STATEMENT_CORRESPONDENCE.md.