The blog post discusses a recent proof by OpenAI regarding the Navier-Stokes equations in fluid dynamics, highlighting an overlooked aspect: the formal proof released in Lean 4. The author reflects on the significance of this new contribution amidst ongoing discussions in the field.