bluesky — Kiran — 16 Sep 2026
speaking to an applied mathematician friend at work, the OpenAI NS proof is non-constructive, so while the counter-examp…
#navier-stokes #proof-formalization #constructive-mathematics
speaking to an applied mathematician friend at work, the OpenAI NS proof is non-constructive, so while the counter-example has been proven to exist, it's actually non-trivial to simulate it.
I wonder if porting it (via dedukti?) to Agda might be a valuable thing to do?