On the Navier–Stokes Millennium Prize Problem

La comunidad de OpenAI ha compartido una solución generada por inteligencia artificial al problema del milenio de Navier–Stokes, incluyendo un resumen y una prueba formal en Lean.