OpenAI publicó una solución generada por IA al problema del milenio de Navier–Stokes, con un writeup y una prueba formal en Lean: On the Navier–Stokes Millennium Prize Problem. La cobertura de Latent Space reporta que el resultado salió de una corrida de alrededor de 10.000 agentes colaborando, con cifras de tiempo y cómputo enormes. Y ya hay disputa: un matemático de NYU acusa a OpenAI de haber jugado sucio sobre un problema que hace carreras, según TechCrunch.
Por qué importa
El titular es la matemática. La señal es otra: la prueba está en Lean. Eso significa que el resultado no depende de que le creamos al modelo. Un verificador determinista lo chequea, y ahí se termina la discusión sobre si el output alucinó o no.
Esa es la parte que me interesa como dev, y es la que casi nadie está mirando. Durante dos años el debate fue "¿confío en lo que me genera?". Acá el debate desaparece, porque hay un oráculo externo que dice sí o no. El modelo genera, el verificador juzga. No hay opinión en el medio.
La otra mitad de la señal es incómoda: según lo reportado por Latent Space, esto se logró tirando una cantidad de cómputo paralelo que ninguno de nosotros va a tener. No fue un modelo más inteligente resolviendo el problema de una. Fue una cantidad brutal de intentos, organizados por los propios agentes, contra un juez que filtra. Eso no es magia: es búsqueda a escala con verificación barata.
Qué cambia en la práctica
El patrón se puede copiar sin tener 10.000 agentes. La pregunta que hay que hacerse antes de delegar una tarea a un modelo ahora es una sola: ¿tengo un verificador automático para esto?
Si la respuesta es sí, podés subir muchísimo la agresividad de la delegación, porque el costo de un intento fallido es cero: lo descarta la máquina, no vos leyendo un diff. Si la respuesta es no, seguís siendo vos el cuello de botella y toda la velocidad que ganás generando la perdés revisando.
┌──────────────┐ genera ┌──────────────┐
│ Modelo │ ──────────► │ Candidato │
└──────────────┘ └──────┬───────┘
▲ │
│ reintenta ▼
│ ┌──────────────┐
└───────── no ────────│ Verificador │
└──────┬───────┘
│ sí
▼
┌──────────────┐
│ Revisión │
│ humana │
└──────────────┘El verificador no tiene que ser Lean. En un proyecto real ya lo tenés a mano y probablemente lo estés desaprovechando:
- El compilador. TypeScript en modo estricto rechaza una enorme cantidad de output inválido antes de que lo leas.
- La suite de tests, cuando los tests los escribiste vos y no los generó el mismo modelo que escribe la implementación.
- Los property-based tests, que son lo más parecido a una prueba formal que vas a tener sin cambiar de lenguaje.
- El linter, el typechecker y las validaciones de esquema en los bordes.
La consecuencia de arquitectura es directa: invertir en verificabilidad rinde más que invertir en prompts. Un tipado fuerte, contratos explícitos en los límites del sistema y tests deterministas no son solo higiene: son lo que habilita delegar en serio.
Cuándo NO usarlo
Acá va lo honesto, porque el entusiasmo de esta semana va a hacer mucho daño.
| Situación | ¿Delegar en volumen? | Por qué |
|---|---|---|
| Refactor con tests sólidos previos | Sí | El verificador es real y es tuyo |
| Feature nueva sin especificación clara | No | No hay contra qué verificar |
| Tests generados por el mismo modelo | No | El juez y el acusado son la misma persona |
| Decisiones de producto o de UX | No | No existe verificador automático |
| Código con efectos externos irreversibles | No | Un intento fallido no cuesta cero |
Tres límites concretos:
El costo no es un detalle. Latent Space reporta una corrida con miles de agentes y una cifra de cómputo que ubica esto muy lejos del presupuesto de cualquier equipo normal. Trasladar esa estrategia a un sprint sin medir gasto es la forma más rápida de quemar plata. El patrón se copia; la escala no.
Sin verificador, el paralelismo empeora las cosas. Diez candidatos sin juez automático no son diez chances de acertar: son diez cosas que tenés que leer. La búsqueda masiva solo sirve cuando filtrar es más barato que generar.
La disputa de autoría no es ruido. El artículo de TechCrunch describe un conflicto sobre un problema que define carreras. Traducido a nuestro terreno: cuando el output de un sistema automático entra a un repo compartido, la pregunta de quién responde por ese código deja de ser filosófica. Si tu equipo todavía no tiene una respuesta a eso, no la resuelvas después del incidente.
Y algo que el material provisto no permite afirmar: no hay confirmación de que la comunidad matemática haya aceptado el resultado ni de que el premio esté adjudicado. La verificación en Lean es fuerte, pero la aceptación de un resultado de este calibre lleva tiempo. Cualquiera que hoy te diga que el problema está cerrado está yendo más rápido que la evidencia disponible.
Qué haría hoy
Nada dramático. Lo que sí haría es una auditoría de media hora sobre el proyecto en el que estoy: dónde tengo verificación automática real y dónde estoy fingiendo que la tengo. Ese mapa te dice exactamente qué podés delegar mañana y qué no.
Y donde falte, invertiría ahí antes que en cualquier otra cosa relacionada con IA. Tipos más estrictos, contratos en los bordes, tests que no dependan del azar. No porque estén de moda, sino porque son la única infraestructura que convierte un modelo en algo que trabaja para vos en vez de darte trabajo.
El resto —los 10.000 agentes, los 88 horas, el millón de dólares— es de ellos. La lección es nuestra y es bastante más aburrida: el que tiene mejor verificador, gana.