OpenAI’s Navier-Stokes release included a Lean 4 formal proof

When OpenAI released their proof that solutions to the Navier-Stokes equations can blow up in finite time, they also released a formal proof in Lean 4.