Una de les grans preguntes obertes de la física matemàtica és si les equacions que descriuen el moviment dels fluids poden, partint de condicions perfectament suaus i raonables, generar en algun moment una singularitat: un punt on una magnitud es dispara cap a l'infinit en un temps finit. És la pregunta de fons darrere del problema del mil·lenni de Navier-Stokes, i en els darrers anys els matemàtics Diego Córdoba i Luis Martínez-Zoroa havien obert una via per construir aquest tipus d'«explosions» quan s'hi afegeix una força externa que empeny el sistema.
El matemàtic Tristan Buckmaster, professor a la Universitat de Nova York, i l'investigador Levent Alpöge han fet públics aquest setembre tres resultats que completen aquest programa per a l'equació del medi porós incompressible, l'equació de Boussinesq en dues dimensions i, la més esperada, les equacions d'Euler incompressibles en tres dimensions: en tots tres casos, construeixen una força externa i una dada inicial suaus que produeixen una singularitat en temps finit, i les demostracions centrals han quedat verificades formalment amb l'assistent de proves Lean, que comprova que no hi ha cap forat lògic en la cadena d'inferències. Terence Tao, un dels matemàtics de referència mundial en aquest camp, ha confirmat i comentat els resultats al seu blog l'endemà.
El treball s'ha fet amb una assistència molt intensiva de models d'IA, principalment Claude, d'Anthropic, i eines basades en Codex, d'OpenAI, per generar candidats de demostració que Buckmaster i Alpöge han hagut de revisar, corregir i reescriure manualment; els mateixos autors han admès públicament que la primera versió del text era, en paraules seves, «la pitjor redacció que hem vist mai en la història de les matemàtiques» abans de polir-la fins a un nivell publicable. És rellevant perquè és un dels primers casos en què un resultat matemàtic d'aquesta ambició, tocant de prop el problema de Navier-Stokes, combina IA generativa i verificació formal en el mateix procés, en lloc de fer-los servir per separat.
Els resultats encara no han passat una revisió per parells tradicional més enllà de la verificació formal en Lean, que garanteix la correcció lògica de la demostració però no substitueix l'escrutini de la comunitat matemàtica sobre la seva rellevància i les seves implicacions; a més, els casos resolts inclouen una força externa artificial que ajuda a generar la singularitat, de manera que el problema original de Navier-Stokes sense forçament extern, el que té el premi del mil·lenni associat, continua obert. La publicació ha anat acompanyada d'una disputa pública sobre l'autoria i el crèdit del treball, amb Buckmaster acusant OpenAI d'haver-lo pressionat per deixar Alpöge, empleat d'Anthropic, fora de la publicació.