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, muchos de ellos, aunque no todos, acompañados de formalizaciones en 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 un modelo interno que OpenAI no ha publicado ni nombrado.
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 publicar 722 manuscritos en una sola liberación, solo una parte con verificación formal por ordenador, todos sobre problemas de investigación abiertos. 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 —17 campos que van de la teoría de números a las álgebras de operadores, con incursiones en informática teórica y física— que no son terreno de entrenamiento estándar. Muchas demostraciones incluyen el archivo Lean que las formaliza, pero no todas: el propio README advierte de que algunos resultados no formalizados podrían tener problemas.
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 precedente de Navier-Stokes
En septiembre de 2026, OpenAI ya había anunciado que un modelo interno sin publicar había obtenido un resultado sobre 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.
Ese resultado todavía no está validado —el proceso de validación en matemáticas de frontera puede durar meses— pero el hecho de que OpenAI haya podido producir 722 manuscritos adicionales 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. Andrew Sutherland, matemático del MIT, ha advertido de que cabe esperar que algunas demostraciones contengan errores, posiblemente graves, y pide tratar como no verificados estos resultados hasta que el modelo se publique y puedan replicarse.
El AGMAI —el grupo asesor sobre matemáticas e IA alojado en el Institute for Advanced Study de Princeton— ha advertido de que su papel consultivo no debe interpretarse como un juicio sobre el impacto de estos resultados, y de que esta publicación es el principio, no el final, del trabajo.
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 expertos en IA de Estados Unidos ve positivo su impacto en el empleo, frente a solo el 23% del público. 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.