OpenAI ha subido a GitHub el mayor repositorio de demostraciones matemáticas generadas por inteligencia artificial jamás publicado: 722 manuscritos agrupados en 372 familias de teoremas, todos verificados formalmente con Lean, el asistente de pruebas que la comunidad matemática usa para confirmar que un argumento no tiene fisuras lógicas. El repositorio está disponible en github.com/openai/math desde el 7 de octubre de 2026 y fue producido con el mismo modelo que en julio resolvió un problema abierto de las ecuaciones de Navier-Stokes.
El número importa por contexto: la base de datos Lean 4 Mathlib —la mayor biblioteca pública de matemáticas formalizadas construida por la comunidad— tiene alrededor de 200.000 teoremas acumulados en varios años de trabajo colaborativo. OpenAI acaba de añadir 722 demostraciones nuevas en una sola liberación, todas verificadas por ordenador, todas en problemas de investigación activa. No es una colección de ejercicios de bachillerato.
¿Qué hay exactamente en el repositorio y cómo se generó?
Los 722 manuscritos cubren áreas de la matemática pura contemporánea —teoría de números analítica, álgebra conmutativa, topología diferencial y geometría algebraica— que no son terreno de entrenamiento estándar. Cada demostración incluye el archivo Lean que la verifica, la prueba en lenguaje matemático natural y las referencias a los teoremas previos de los que depende.
El proceso de generación usa tiempo de cómputo real: cada resultado consume aproximadamente tres horas de ChatGPT Pro en modo de razonamiento extendido. Para las 722 demostraciones, eso son más de 2.100 horas de cómputo acumulado. OpenAI no ha revelado el coste en infraestructura, pero a los precios actuales de sus propios servicios estamos hablando de varias decenas de miles de dólares solo en inferencia.
Desde 2022 llevo siguiendo los avances en IA matemática, desde el primer AlphaCode hasta los trabajos de razonamiento simbólico de DeepMind. Lo que me parece diferente aquí no es el número de problemas —es la verificación formal. Un LLM puede «demostrar» algo que parece correcto en lenguaje natural pero que tiene un error sutil en el paso 4. Lean no permite eso: o es riguroso o el checker lo rechaza.
El modelo que ya resolvió Navier-Stokes vuelve a sorprender
El sistema de OpenAI que generó este corpus es el mismo que en julio de 2026 publicó una solución a uno de los problemas abiertos de las ecuaciones de Navier-Stokes para fluidos incompresibles en tres dimensiones —uno de los siete Problemas del Milenio del Clay Mathematics Institute, con un premio de un millón de dólares asociado.
Esa solución todavía está en revisión por pares —el proceso de validación en matemáticas de frontera puede durar meses— pero el hecho de que OpenAI haya podido producir 722 demostraciones adicionales verificadas formalmente desde entonces sugiere que el modelo tiene consistencia, no fue un golpe de suerte.
La conexión con la tesis de que 2026 es el año del agente de IA general es directa: un agente que puede hacer matemáticas de investigación verificadas formalmente no es una herramienta de asistencia —es un colaborador científico. La pregunta ya no es si puede hacerlo, sino qué tipo de supervisión humana tiene sentido aplicar.
¿Es esto ciencia verificable o un artefacto estadístico muy sofisticado?
La objeción más seria viene de los propios matemáticos. Tristan Buckmaster, de la Universidad de Princeton y especialista en ecuaciones diferenciales parciales, ha publicado en arXiv una nota preliminar cuestionando el alcance real de la contribución de Navier-Stokes. Su argumento: el modelo podría estar construyendo argumentos válidos formalmente pero que no abordan la esencia profunda del problema, demostrando versiones técnicamente más simples que las que la comunidad considera el núcleo de la pregunta abierta.
El equipo asesor de AGMAI —la coalición de institutos matemáticos que supervisa la evaluación de la solución de Navier-Stokes— ha emitido una advertencia similar: la verificación por Lean confirma que la lógica es consistente, no que el resultado sea matemáticamente interesante o que responda la pregunta de fondo.
La fiebre de los agentes de IA y las barandillas que todavía le faltan a la web aplica aquí con precisión: tenemos la capacidad técnica antes que los marcos de evaluación. ¿Quién decide si una demostración matemática producida por IA merece crédito de autoría? ¿Cómo cita la comunidad resultados de un modelo propietario que podría desaparecer o cambiar en la próxima actualización?
¿Cuándo los matemáticos dejan de ser los únicos árbitros de las matemáticas?
El AI Index 2026 de Stanford y la brecha entre expertos y ciudadanos sobre IA documenta que el 73% de los especialistas técnicos cree que la IA mejorará la investigación científica, mientras que solo el 23% del público general opina lo mismo. Las 722 demostraciones de OpenAI son el tipo de evidencia que mueve esa brecha —en una dirección o en otra, según cómo se lea.
Mi lectura es esta: el corpus es un logro técnico real y la verificación formal con Lean es el elemento que lo separa de la ficción. Pero los matemáticos tienen razón al insistir en que verificación formal no equivale a comprensión. Lo que OpenAI ha conseguido es acelerar una parte del trabajo matemático —la construcción y chequeo de argumentos— que hasta ahora era puramente humana. No ha conseguido, todavía, reemplazar la intuición sobre qué problemas merece la pena resolver ni en qué dirección buscar. Esa intuición es, quizá, lo más parecido a lo que llamamos matemática de verdad.