Credit & pins
Provenance
Upstream credit, licences and commit pins. The site renders numbers from these sources, never from hand-entry.
Upstream mathematics
The mathematics and the Lean formalization of the blow-up are OpenAI’s: openai/NavierStokesAndEuler at commit f9e8bc5b38b6e212696e8a30e3e91517af887bbd (Apache-2.0). Toolchain: Lean 4.34.1, Mathlib d13f23b.
Pinned source commits
| Repository | Pinned commit |
|---|---|
| kts-global/lean-proofs-public | 3ccc9f72e7038a6a990a2d21b9305c2787f24b21 |
| kts-global/lean-proofs-navier-stokes-cd | 9f3df6786654ffdcfd87e9d324b58f924e60f7c6 |
| kts-global/lean-proofs-tao-shortbound-global-regularity | 952d19cdaf3b33f27cd23e322607c18cd20b7fc3 |
Licences
Upstream and third-party files keep their own licences (Apache-2.0). Files added by KTS Global are published under Apache-2.0. The CHAOS implementation is not distributed or licensed by these packages.