Didn't OpenAI make a Lean proof? https://github.com/openai/NavierStokesAndEuler/tree/main/Nav... "This repository contains Lean 4 formalizations of the results presented in “Finite time blowup for Navier–Stokes” and “Finite time blowup for the Euler equation” by OpenAI."