{"node":{"domain":"geometryintelligence.institute","role":"research-evidence","parent":"KTS Global Tier 0"},"owner":{"name":"Tim Jacobs","affiliation":"KTS Global","orcid":"0009-0008-7130-1448"},"upstream":{"repo":"openai/NavierStokesAndEuler","commit":"f9e8bc5b38b6e212696e8a30e3e91517af887bbd","license":"Apache-2.0","url":"https://github.com/openai/NavierStokesAndEuler"},"toolchain":{"lean":"4.34.1","mathlib":"d13f23b723b8a846827a245b89c10fc7d3f11612"},"standard_axioms":["propext","Classical.choice","Quot.sound"],"strip":{"theorems":40986,"closure_modules":620,"kernels":["Lean default","nanoda"],"standard_axioms":3,"axiom_policy_checks_tao":58,"axiom_policy_checks_cd":14},"proofs":[{"id":"gi:proof:s437","slug":"s437","title":"S437: Lean 4.34.1 port and rebuild of OpenAI's NavierStokesAndEuler formalization (Clay alternatives C and D)","status":"Released","conditional":false,"version":"s437-v1","page":"https://geometryintelligence.institute/proofs/s437/","repo":"https://github.com/kts-global/lean-proofs-public","repo_sha":"3ccc9f72e7038a6a990a2d21b9305c2787f24b21","doi":"10.5281/zenodo.23448690","wikidata":"Q141761720","lean_names":["NavierStokes.Comparator.navier_stokes_breakdown_R3","NavierStokes.Comparator.navier_stokes_breakdown_periodic"],"metrics":{"modules_edited":21,"kernels_checked":["Lean default","nanoda"],"challenge_statements":"unchanged from upstream"},"axioms":["propext","Classical.choice","Quot.sound"]},{"id":"gi:proof:r2r3","slug":"r2-r3","title":"Navier–Stokes R2/R3 community verification package, V1","status":"Released","conditional":false,"version":"r2-r3-v1","page":"https://geometryintelligence.institute/proofs/r2-r3/","repo":"https://github.com/kts-global/lean-proofs-public","repo_sha":"3ccc9f72e7038a6a990a2d21b9305c2787f24b21","doi":"10.5281/zenodo.23535805","wikidata":"Q141803373","lean_names":["ClayFefferman","ClayFeffermanViaD","NavierStokesComplete","ClayC","ClayD"],"metrics":{"theorems":40986,"closure_modules":620,"comparator_exit0":["ClayFefferman","ClayFeffermanViaD","NavierStokesComplete","ClayC","ClayD"],"verification":"publisher-executed, native Ubuntu 24.04 x86_64","wall_seconds":5678},"axioms":["propext","Classical.choice","Quot.sound"]},{"id":"gi:proof:nscd","slug":"navier-stokes-cd","title":"Lean 4 - Proof - Navier–Stokes C/D (KTS Global)","status":"Released","conditional":false,"version":"1.0.0","page":"https://geometryintelligence.institute/proofs/navier-stokes-cd/","repo":"https://github.com/kts-global/lean-proofs-navier-stokes-cd","repo_sha":"9f3df6786654ffdcfd87e9d324b58f924e60f7c6","doi":null,"wikidata":null,"lean_names":["NavierStokes.ClayC.clay_C","NavierStokes.ClayD.clay_D","NavierStokes.ClayChallenge.clay_navier_stokes_fefferman","NavierStokes.ClayChallenge.clay_navier_stokes_fefferman_via_D","NavierStokes.Comparator.navier_stokes_clay_via_C","NavierStokes.Comparator.navier_stokes_clay_via_D"],"metrics":{"shipped_modules":620,"navierstokes_lean_files":613,"claystatement_lean_files":6,"declarations_verified":12,"targets":6,"bridges":6,"axiom_policy_checks":14,"ecr_class":"LIBRARY_SUPPORT","mutation_tests":"5 wrong/weakened statements + inserted sorry rejected","non_vacuity":["CDNonVacuity.zero_solR3","CDNonVacuity.zero_solTorus"],"builder_authored_not_claimed":["CDVerification.lean","CDNonVacuity.lean"]},"axioms":["propext","Classical.choice","Quot.sound"]},{"id":"gi:proof:tao-shortbound","slug":"tao-shortbound","title":"Lean 4 - Proof - Tao ShortBound to Global Regularity","status":"Release candidate","conditional":true,"version":"0.1.0","page":"https://geometryintelligence.institute/proofs/tao-shortbound/","repo":"https://github.com/kts-global/lean-proofs-tao-shortbound-global-regularity","repo_sha":"952d19cdaf3b33f27cd23e322607c18cd20b7fc3","doi":null,"wikidata":null,"lean_names":["OpenObligations.Torus.Tao.core_global_of_shortBound"],"metrics":{"jobs":8959,"errors":0,"unproved_declaration_warnings":0,"declarations":47,"theorems":36,"definitions":11,"ecr_checks":11,"axiom_policy_checks":58,"audit_constants":544,"audit_theorems":384,"token_scan_hits":0,"token_scan_files":35,"ecr_battery":"36/36","mutation_tests":"4/4","non_vacuity":"proved in Lean (TaoShortBound/ECR.lean)","ecr_result_entries":36},"axioms":["propext","Classical.choice","Quot.sound"]}]}